git.iko.soy/Idris-dev
on 019faba help sign in
Idris-dev/decls.mi
40 lines 842 B history raw
1infixl 5 +, - ;
2infixl 6 *, / ;
4infixr 7 :: ;
6data Nat = O | S Nat;
7data List a = Nil | Cons a (List a);
9data Vect : Set -> Nat -> Set where
10 VNil : Vect a O
11 | (::) : a -> Vect a k -> Vect a (S k);
13data Env : Vect Set n -> Set where
14 Empty : Env VNil
15 | Extend : {xs : Vect Set n} -> a -> Env xs -> Env (a :: xs);
17PLUSTY : Set;
18PLUSTY = Nat -> Nat -> Nat;
20plus : PLUSTY;
21plus O y = y;
22plus (S k) y = S (plus k y);
24app : Vect a n -> Vect a m -> Vect a (plus n m);
25app VNil ys = ys;
26app (x :: xs) ys = x :: app xs ys;
28map : (a -> b) -> Vect a n -> Vect b n;
29map f VNil = VNil;
30map f (x :: xs) = f x :: map f xs;
32test : Nat -> Vect Nat (S (S O));
33test n = n :: n :: VNil;
35tvect : Vect Nat (S (S (S (S O))));
36tvect = app (test O) (test (S O));
38mapPlus : Vect Nat n -> Vect Nat n;
39mapPlus = map (plus (S (S O)));