Commit 31094ffb authored by MARCHE Claude's avatar MARCHE Claude

CE: new example on lists (no CE generated yet, to fix)

parent 374fe4df
module List_int
use import int.Int
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
use import list.List
use import list.Length
goal g1: forall l:list int. length l <> 0
goal g2: forall l:list int. length l <> 1
end
\ No newline at end of file
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment