git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/basic017/basic017a.idr
15 lines 418 B history raw
1%auto_implicits off
3data Vect : Nat -> Type -> Type where
4 Nil : {a : _} -> Vect Z a
5 (::) : {a, k : _} -> a -> Vect k a -> Vect (S k) a
7data Elem : {a, n : _} -> a -> Vect n a -> Type where
8 Here : {x, xs : _} -> Elem x (x :: xs)
9 There : {x, y, xs : _} -> Elem x xs -> Elem x (y :: xs)
11append : Vect n a -> Vect m a -> Vect (n + m) a
12append [] ys = ys
13append (x :: xs) ys = x :: append xs ys