Typed

parent 69e4cd37
......@@ -88,11 +88,12 @@ andN̂ k = Mkℂ̂ ⦃ ⇕Vec {k} ⦄ (andN k)
%</andN-typed>
-- TODO: | Vn | = (n * 1) vs. ripple (sized) input has n
%<*ripple-typed>
\AgdaTarget{ripplê}
\begin{code}
ripplê : ∀ n → let Vn = Vec Bool n in Ĉ B₃ (Bool × Vn × Vn) (Vn × Bool)
ripplê n = Mkℂ̂ ⦃ ⇕× {1} ⦃ β̂ = ⇕× ⦃ ⇕Vec {n} ⦄ ⦃ ⇕Vec {n} ⦄ ⦄ ⦄ ⦃ ⇕× ⦃ ⇕Vec {n} ⦄ ⦄ (ripple n)
--ripplê : ∀ n → let Vn = Vec Bool n in Ĉ B₃ (Bool × Vn × Vn) (Vn × Bool)
--ripplê n = Mkℂ̂ ⦃ ⇕× {1} ⦃ β̂ = ⇕× ⦃ ⇕Vec {n} ⦄ ⦃ ⇕Vec {n} ⦄ ⦄ ⦄ ⦃ ⇕× ⦃ ⇕Vec {n} ⦄ ⦄ (ripple n)
\end{code}
%</ripple-typed>
......@@ -149,13 +150,11 @@ haddSpeĉ a b = (a ∧ b) , (a xor b)
\end{code}
%</haddSpec>
-- TODO
%<*proofHaddBool>
\AgdaTarget{proofHaddBool̂}
\begin{code}
proofHaddBool̂ : ∀ a b → ⟦ hadd̂ ⟧̂ (a , b) ≡ haddSpeĉ a b
proofHaddBool̂ a b = cong (_,_ (a ∧ b)) (⊻ℂ̂-proof-subfunc a b)
\end{code}
%</proofHaddBool>
......@@ -175,9 +174,9 @@ faddSpeĉ true true true = true , true
%</faddSpec>
-- TODO
%<*proofFaddBool>
\AgdaTarget{proofFaddBool̂}
\begin{code}
proofFaddBool̂ : ∀ a b c → ⟦ fadd̂ ⟧̂ ((a , b) , c) ≡ faddSpeĉ a b c
proofFaddBool̂ true true true = refl
proofFaddBool̂ true true false = refl
......@@ -187,7 +186,6 @@ proofFaddBool̂ false true true = refl
proofFaddBool̂ false true false = refl
proofFaddBool̂ false false true = refl
proofFaddBool̂ false false false = refl
\end{code}
%</proofFaddBool>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment