Add prelude.fin module
commit62ea7f861d24c8f0e78eff9dc48e5d58686b153e
authorEdwin Brady <eb@cs.st-andrews.ac.uk>
dateSat 7 Jan 2012, 23:30 (15 years ago)
parentb20f2f8
lib/prelude.idr+1
@@ -5,6 +5,7 @@ import io
55
66import prelude.cast
77import prelude.nat
8+import prelude.fin
89import prelude.list
910import prelude.maybe
1011import prelude.either
lib/prelude/fin.idrnew file+13
@@ -0,0 +1,13 @@
1+module prelude.fin
2+
3+import prelude.nat
4+
5+data Fin : Nat -> Set where
6+ fO : Fin (S k)
7+ fS : Fin k -> Fin (S k)
8+
9+instance Eq (Fin n) where
10+ fO == fO = True
11+ (fS k) == (fS k') = k == k'
12+ _ == _ = False
13+
lib/prelude/vect.idr+1−9
@@ -1,18 +1,10 @@
11module prelude.vect
22
33import prelude.nat
4+import prelude.fin
45
56%access public
67
7−data Fin : Nat -> Set where
8− fO : Fin (S k)
9− fS : Fin k -> Fin (S k)
10−
11−instance Eq (Fin n) where
12− fO == fO = True
13− (fS k) == (fS k') = k == k'
14− _ == _ = False
15−
168infixr 7 ::
179
1810data Vect : Set -> Nat -> Set where