{-# OPTIONS --safe --cubical #-}

module Spartan6.Prelude where

open import Cubical.Foundations.Prelude public
open import Cubical.Data.Bool public
  using (Bool; false; true; not; _and_; _or_; _⊕_; if_then_else_)
open import Cubical.Data.FinData public
  using (Fin)
  renaming (zero to fzero; suc to fsuc)
open import Cubical.Data.List public
  using (List)
  renaming
    ([] to []ᴸ; _∷_ to _∷ᴸ_; _++_ to _++ᴸ_;
     map to mapList; foldr to foldrList; length to lengthList)
open import Cubical.Data.Maybe public
  using (Maybe; nothing; just)
open import Cubical.Data.Nat public
  using (ℕ; zero; suc; _+_; _·_; _^_)
open import Cubical.Data.Sigma public
  using (Σ; Σ-syntax; _,_; fst; snd; _×_)
open import Cubical.Data.Sum public
  using (_⊎_; inl; inr)
open import Cubical.Data.Unit public
  using (Unit; tt)
open import Cubical.Data.Vec public
  using (Vec; []; _∷_; map; replicate; lookup; zipWith; foldr)

open import Agda.Builtin.String public using (String)

Bit : Type₀
Bit = Bool

Word : ℕ → Type₀
Word = Vec Bit

low high : Bit
low = false
high = true

mux : Bit → Bit → Bit → Bit
mux select when-false when-true =
  if select then when-true else when-false

mux-low : ∀ x y → mux low x y ≡ x
mux-low x y = refl

mux-high : ∀ x y → mux high x y ≡ y
mux-high x y = refl