@@ -6,7 +6,10 @@ import Prelude.Uninhabited
66
77%default total
88
9−||| Numbers strictly less than some bound. The name comes from "finite sets"
9+||| Numbers strictly less than some bound. The name comes from "finite sets".
10+|||
11+||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
12+||| exceedingly inefficient at run time.
1013||| @ n the upper bound
1114data Fin : (n : Nat) -> Type where
1215 fZ : Fin (S k)
@@ -24,16 +27,19 @@ instance Eq (Fin n) where
2427 (==) (fS k) (fS k') = k == k'
2528 (==) _ _ = False
2629
30+||| There are no elements of `Fin Z`
2731FinZAbsurd : Fin Z -> _|_
2832FinZAbsurd fZ impossible
2933
3034FinZElim : Fin Z -> a
3135FinZElim x = FalseElim (FinZAbsurd x)
3236
37+||| Convert a Fin to a Nat
3338finToNat : Fin n -> Nat
3439finToNat fZ = Z
3540finToNat (fS k) = S (finToNat k)
3641
42+||| `finToNat` is injective
3743finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
3844finToNatInjective fZ fZ refl = refl
3945finToNatInjective (fS m) fZ refl impossible
@@ -44,6 +50,7 @@ finToNatInjective (fS m) (fS n) prf =
4450instance Cast (Fin n) Nat where
4551 cast x = finToNat x
4652
53+||| Convert a Fin to an Integer
4754finToInteger : Fin n -> Integer
4855finToInteger fZ = 0
4956finToInteger (fS k) = 1 + finToInteger k
@@ -123,9 +130,13 @@ natToFin _ _ = Nothing
123130integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
124131integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
125132
133+||| Proof that some `Maybe` is actually `Just`
126134data IsJust : Maybe a -> Type where
127135 ItIsJust : IsJust {a} (Just x)
128136
137+||| Allow overloading of Integer literals for Fin.
138+||| @ x the Integer that the user typed
139+||| @ prf an automatically-constructed proof that `x` is in bounds
129140fromInteger : (x : Integer) ->
130141 {default ItIsJust
131142 prf : (IsJust (integerToFin x n))} ->