git.iko.soy/Idris-dev
on 019faba help sign in
Idris-dev/test.mi
29 lines 767 B history raw
1data N : Set 0 where
2 | O : N
3 | S : N -> N;
5one : N = S O;
6two : N = S (S O);
7three : N = S two;
9plus : N -> N -> N;
11data Parity : N -> Set where
12 | even : (n:N) -> (Parity (plus n n))
13 | odd : (n:N) -> (Parity (S (plus n n)));
15data Vect : (A:Set 0) -> (n:N) -> Set 0 where
16 | Nil : (A:Set 0) -> (Vect A O)
17 | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));
19vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);
20vappend : (A:Set) -> (m:N) -> (n:N) -> (Vect A m) -> (Vect A n) -> (Vect A (plus m n));
21vadd : (m:N) -> (Vect N m) -> (Vect N m) -> (Vect N m);
23data Infer : Set 0 where
24 | MkInf : (A : Set) -> A -> Infer;
26data PClause : Set 0 where
27 | MkP : (A : Set) -> A -> A -> PClause;
29npar : (n:N) -> (p:Parity n) -> N;