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