test-ind.why 269 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17

theory T

type list 'a = Nil | Cons 'a (list 'a)

function app (l1:list 'a) (l2:list 'a) : (list 'a) =
  match l1 with
  | Nil -> l2
  | Cons x r -> Cons x (app r l2) 
  end

lemma app_nil : forall l:list 'a. app l Nil = l

type tree = Leaf int | Node tree tree

end