Commit ed27a8f4 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

make bench passe

parent 01b552e6
......@@ -9,12 +9,12 @@ theory IntList
logic sorted(int list)
axiom Sorted_nil :
sorted(nil)
sorted(Nil)
axiom Sorted_one :
forall x: int. sorted(cons(x, nil))
forall x: int. sorted(Cons(x, Nil))
axiom Sorted_cons:
forall x,y: int. forall l: int list.
sorted(cons(y, l)) -> x <= y -> sorted(cons(x, cons(y, l)))
sorted(Cons(y, l)) -> x <= y -> sorted(Cons(x, Cons(y, l)))
end
......
(***
theory Set_list
use open List
use import List
logic add(x:'a,s:'a t) : 'a t = Cons(x,s)
logic mem(x:'a,s:'a t) = match s with
| Nil -> false
......@@ -39,4 +40,5 @@ theory Set_array
use include Set_array
end
\ No newline at end of file
end
***)
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