git.iko.soy/Idris-dev
on ffd5e72 help sign in
Idris-dev/src/test.mi
13 lines 303 B history raw
1N : Set 0;
2O : N;
3S : N -> N;
5one : N = S O;
6two : N = S (S O);
7three : N = S two;
9data Vect : (A:Set 0) -> (n:N) -> Set 0 where
10 Nil : (A:Set 0) -> (Vect A O)
11 | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));
13vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);