git.iko.soy/Idris-dev
on 64b7cfd help sign in
Idris-dev/decls.mi
25 lines 444 B history raw
1infixl 5 +, - ;
2infixl 6 *, / ;
4infixl 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);
13plus : Nat -> Nat -> Nat;
14{-
15plus O y = y;
16plus (S k) y = S (plus k y);
17-}
19app : Vect a n -> Vect a m -> Vect a (plus n m);
20{-
21app VNil ys = ys;
22app (x :: xs) ys = x :: (app xs ys);
23-}
25(::) : a -> Vect a k -> Vect a (S k);