@@ -3,6 +3,8 @@ module Prelude.Fin
3import Prelude.Nat
3import Prelude.Nat
4import Prelude.Either
4import Prelude.Either
6data Fin : Nat -> Type where
8data Fin : Nat -> Type where
7 fZ : Fin (S k)
9 fZ : Fin (S k)
8 fS : Fin k -> Fin (S k)
10 fS : Fin k -> Fin (S k)
@@ -12,19 +14,19 @@ instance Eq (Fin n) where
12 (==) (fS k) (fS k') = k == k'
14 (==) (fS k) (fS k') = k == k'
13 (==) _ _ = False
15 (==) _ _ = False
15−finToNat : Fin n -> Nat -> Nat
17+finToNat : Fin n -> Nat
16−finToNat fZ a = a
18+finToNat fZ = Z
17−finToNat (fS x) a = finToNat x (S a)
19+finToNat (fS k) = S (finToNat k)
19instance Cast (Fin n) Nat where
21instance Cast (Fin n) Nat where
20− cast x = finToNat x Z
22+ cast x = finToNat x
22−finToInt : Fin n -> Integer -> Integer
24+finToInteger : Fin n -> Integer
23−finToInt fZ a = a
25+finToInteger fZ = 0
24−finToInt (fS x) a = finToInt x (a + 1)
26+finToInteger (fS k) = 1 + finToInteger k
26instance Cast (Fin n) Integer where
28instance Cast (Fin n) Integer where
27− cast x = finToInt x 0
29+ cast x = finToInteger x
29weaken : Fin n -> Fin (S n)
31weaken : Fin n -> Fin (S n)
30weaken fZ = fZ
32weaken fZ = fZ