Mercurial > hg > Members > kono > Proof > category

comparison negnat.agda @ 454:2f07f4dd9a6d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 13:25:05 +0900
parents 3c2ce4474d92
children 4c0580d9dda4
comparison
equal deleted inserted replaced
453:3c2ce4474d92 454:2f07f4dd9a6d
59 bad : Fin 0 → ⊥ 59 bad : Fin 0 → ⊥
60 bad = Fin-elim (λ n _ → Nope0 n) (λ _ → _) _ 60 bad = Fin-elim (λ n _ → Nope0 n) (λ _ → _) _
61 61
62 62
63 -- http://stackoverflow.com/questions/18347542/agda-how-does-one-obtain-a-value-of-a-dependent-type 63 -- http://stackoverflow.com/questions/18347542/agda-how-does-one-obtain-a-value-of-a-dependent-type
64
65 even : ℕ -> Set 64 even : ℕ -> Set
66 even zero = ⊤ 65 even zero = ⊤
67 even (suc zero) = ⊥ 66 even (suc zero) = ⊥
68 even (suc (suc n)) = even n 67 even (suc (suc n)) = even n
69 68