module IEEE754.Prelude where

open import Cubical.Foundations.Prelude public

open import Cubical.Data.Bool public
  using (Bool; true; false; not; _and_; _or_; if_then_else_; Bool→Type)
open import Cubical.Data.FinData public
  using (Fin)
open import Cubical.Data.Nat public
  using (ℕ; zero; suc; _+_; _·_; _^_; NonZero)
open import Cubical.Data.Rationals public
  using (ℚ; isSetℚ)
open import Cubical.Data.Sigma public
  using (Σ; _×_; _,_; fst; snd)
open import Cubical.Data.Unit public
  using (Unit; tt)
open import Cubical.Data.Vec public
  using (Vec; []; _∷_; head; tail; map; replicate; lookup)

Bit : Type₀
Bit = Bool

BitVec : ℕ → Type₀
BitVec n = Vec Bit n

bit0 bit1 : Bit
bit0 = false
bit1 = true

allOnes : ∀ {n} → BitVec n → Bool
allOnes [] = true
allOnes (true ∷ bits) = allOnes bits
allOnes (false ∷ bits) = false

allZeros : ∀ {n} → BitVec n → Bool
allZeros [] = true
allZeros (false ∷ bits) = allZeros bits
allZeros (true ∷ bits) = false

anyOne : ∀ {n} → BitVec n → Bool
anyOne [] = false
anyOne (true ∷ bits) = true
anyOne (false ∷ bits) = anyOne bits