list.mlw 422 Bytes
Newer Older
1 2 3

module List_int

4
  use int.Int
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
  
  type list = Nil | Cons int list
  
  function length (l:list) : int = 
    match l with
    | Nil -> 0
    | Cons _ l -> 1 + length l
    end
   
  goal g1: forall l:list. length l <> 0

  goal g2: forall l:list. length l <> 1
  
end

module List_poly

22 23
  use list.List
  use list.Length
24 25 26 27 28 29
  
  goal g1: forall l:list int. length l <> 0

  goal g2: forall l:list int. length l <> 1
  
end