test-match.why 458 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8


theory T

  use import int.Int

  type list = Nil | Cons int list

9 10 11 12 13 14 15 16 17
  function tl (l:list) : list =
    match l with
       | Nil -> Nil
       | Cons _ r -> r
    end

  goal g0: tl (Cons 42 (Cons 37 Nil)) = Cons 37 Nil

  function length (l:list) : int =
MARCHE Claude's avatar
MARCHE Claude committed
18 19 20 21 22
    match l with
       | Nil -> 0
       | Cons _ r -> 1 + length r
    end

23 24 25
  goal g1 : forall l:list. l <> Nil -> let h = tl l in length l = 1 + length h
 
  goal g2: length (Cons 1 Nil) = 1
MARCHE Claude's avatar
MARCHE Claude committed
26 27 28


end