git.iko.soy/Idris-dev
on master help sign in
Add FinZAbsurd and FinZElim.
d904212Stephen Drodge
libs/prelude/Prelude/Fin.idr+6
compare with master
unifiedsplit
@@ -14,6 +14,12 @@ instance Eq (Fin n) where
14 (==) (fS k) (fS k') = k == k'
14 (==) (fS k) (fS k') = k == k'
15 (==) _ _ = False
15 (==) _ _ = False
16
16
17+FinZAbsurd : Fin Z -> _|_
18+FinZAbsurd fZ impossible
19+
20+FinZElim : Fin Z -> a
21+FinZElim x = FalseElim (FinZAbsurd x)
22+
17finToNat : Fin n -> Nat
23finToNat : Fin n -> Nat
18finToNat fZ = Z
24finToNat fZ = Z
19finToNat (fS k) = S (finToNat k)
25finToNat (fS k) = S (finToNat k)