git.iko.soy/Idris-dev
on master help sign in
Add prelude.fin module
62ea7f8Edwin Brady
lib/prelude.idr+1
compare with master
unifiedsplit
@@ -5,6 +5,7 @@ import io
5
5
6import prelude.cast
6import prelude.cast
7import prelude.nat
7import prelude.nat
8+import prelude.fin
8import prelude.list
9import prelude.list
9import prelude.maybe
10import prelude.maybe
10import prelude.either
11import 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 @@
1module prelude.vect
1module prelude.vect
2
2
3import prelude.nat
3import prelude.nat
4+import prelude.fin
4
5
5%access public
6%access public
6
7
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−
16infixr 7 ::
8infixr 7 ::
17
9
18data Vect : Set -> Nat -> Set where
10data Vect : Set -> Nat -> Set where