Add FinZAbsurd and FinZElim.
commitd904212b92808ea999933a4966c724fe68936277
authorStephen Drodge <stephen.drodge@gmail.com>
dateFri 29 Nov 2013, 17:07 (13 years ago)
parentfadbbc8
libs/prelude/Prelude/Fin.idr+6
@@ -14,6 +14,12 @@ instance Eq (Fin n) where
1414 (==) (fS k) (fS k') = k == k'
1515 (==) _ _ = False
1616
17+FinZAbsurd : Fin Z -> _|_
18+FinZAbsurd fZ impossible
19+
20+FinZElim : Fin Z -> a
21+FinZElim x = FalseElim (FinZAbsurd x)
22+
1723finToNat : Fin n -> Nat
1824finToNat fZ = Z
1925finToNat (fS k) = S (finToNat k)