@@ -3,6 +3,8 @@ module Prelude.Fin
33import Prelude.Nat
44import Prelude.Either
55
6+%default total
7+
68data Fin : Nat -> Type where
79 fZ : Fin (S k)
810 fS : Fin k -> Fin (S k)
@@ -12,19 +14,19 @@ instance Eq (Fin n) where
1214 (==) (fS k) (fS k') = k == k'
1315 (==) _ _ = False
1416
15−finToNat : Fin n -> Nat -> Nat
16−finToNat fZ a = a
17−finToNat (fS x) a = finToNat x (S a)
17+finToNat : Fin n -> Nat
18+finToNat fZ = Z
19+finToNat (fS k) = S (finToNat k)
1820
1921instance Cast (Fin n) Nat where
20− cast x = finToNat x Z
22+ cast x = finToNat x
2123
22−finToInt : Fin n -> Integer -> Integer
23−finToInt fZ a = a
24−finToInt (fS x) a = finToInt x (a + 1)
24+finToInteger : Fin n -> Integer
25+finToInteger fZ = 0
26+finToInteger (fS k) = 1 + finToInteger k
2527
2628instance Cast (Fin n) Integer where
27− cast x = finToInt x 0
29+ cast x = finToInteger x
2830
2931weaken : Fin n -> Fin (S n)
3032weaken fZ = fZ