@@ -6,7 +6,10 @@ import Prelude.Uninhabited
7%default total
7%default total
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".
11+||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
12+||| exceedingly inefficient at run time.
10||| @ n the upper bound
13||| @ n the upper bound
11data Fin : (n : Nat) -> Type where
14data Fin : (n : Nat) -> Type where
12 fZ : Fin (S k)
15 fZ : Fin (S k)
@@ -24,16 +27,19 @@ instance Eq (Fin n) where
24 (==) (fS k) (fS k') = k == k'
27 (==) (fS k) (fS k') = k == k'
25 (==) _ _ = False
28 (==) _ _ = False
30+||| There are no elements of `Fin Z`
27FinZAbsurd : Fin Z -> _|_
31FinZAbsurd : Fin Z -> _|_
28FinZAbsurd fZ impossible
32FinZAbsurd fZ impossible
30FinZElim : Fin Z -> a
34FinZElim : Fin Z -> a
31FinZElim x = FalseElim (FinZAbsurd x)
35FinZElim x = FalseElim (FinZAbsurd x)
37+||| Convert a Fin to a Nat
33finToNat : Fin n -> Nat
38finToNat : Fin n -> Nat
34finToNat fZ = Z
39finToNat fZ = Z
35finToNat (fS k) = S (finToNat k)
40finToNat (fS k) = S (finToNat k)
42+||| `finToNat` is injective
37finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
43finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
38finToNatInjective fZ fZ refl = refl
44finToNatInjective fZ fZ refl = refl
39finToNatInjective (fS m) fZ refl impossible
45finToNatInjective (fS m) fZ refl impossible
@@ -44,6 +50,7 @@ finToNatInjective (fS m) (fS n) prf =
44instance Cast (Fin n) Nat where
50instance Cast (Fin n) Nat where
45 cast x = finToNat x
51 cast x = finToNat x
53+||| Convert a Fin to an Integer
47finToInteger : Fin n -> Integer
54finToInteger : Fin n -> Integer
48finToInteger fZ = 0
55finToInteger fZ = 0
49finToInteger (fS k) = 1 + finToInteger k
56finToInteger (fS k) = 1 + finToInteger k
@@ -123,9 +130,13 @@ natToFin _ _ = Nothing
123integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
130integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
124integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
131integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
133+||| Proof that some `Maybe` is actually `Just`
126data IsJust : Maybe a -> Type where
134data IsJust : Maybe a -> Type where
127 ItIsJust : IsJust {a} (Just x)
135 ItIsJust : IsJust {a} (Just x)
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
129fromInteger : (x : Integer) ->
140fromInteger : (x : Integer) ->
130 {default ItIsJust
141 {default ItIsJust
131 prf : (IsJust (integerToFin x n))} ->
142 prf : (IsJust (integerToFin x n))} ->