blob: f31278f54f08832f00efa7ad1e8ef62c4d752bbc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
import nat ;
data List : (_:Type) -> Type where
{ Nil : (A:Type) -> List A ;
Cons : (A:Type) -> A -> List A -> List A ; } ;
size : (A:Type) -> List A -> Nat ;
size _ (Nil _) = Zero ;
size A (Cons _ x xs) = Succ (size A xs) ;
map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B ;
map _ B _ (Nil _) = Nil B ;
map A B f (Cons _ x xs) = Cons B (f x) (map A B f xs) ;
append : (A:Type) -> (xs:List A) -> List A -> List A ;
append _ (Nil _) ys = ys ;
append A (Cons _ x xs) ys = Cons A x (append A xs ys) ;
|
