Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Managed to prove the path `add[even] <=> eq`
prove_add_even : (x : Nat) -> (y : Nat) -> even (add x y) = eq (even x) (even y)
prove_add_even Z Z = Refl
prove_add_even Z (S Z) = Refl
prove_add_even Z (S (S k)) = prove_add_even Z k
prove_add_even (S Z) Z = Refl
prove_add_even (S (S k)) Z = prove_add_even k Z
prove_add_even (S Z) (S Z) = Refl
prove_add_even (S Z) (S (S k)) = prove_add_even (S Z) k
prove_add_even (S (S k)) (S j) = prove_add_even k (S j)
add_even : SymPath2 Nat Bool
add_even = add[even]^2 <=> eq by prove_add_even
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.