Commit 5619e208 authored by Andrei Paskevich's avatar Andrei Paskevich

theories/{map,set}.why: remove a warning for map extensionality

parent ff48ef0d
......@@ -46,8 +46,10 @@ theory MapExt
predicate (==) (m1 m2: 'a -> 'b) = forall x: 'a. m1 x = m2 x
axiom extensionality:
lemma extensionality:
forall m1 m2: 'a -> 'b. m1 == m2 -> m1 = m2
(* This lemma is actually provable in Why3, because of how
eliminate_epsilon handles equality to a lambda-term. *)
end
......
......@@ -129,7 +129,7 @@ theory Set
*)
clone export SetGen with type set = set,
predicate mem = mem, axiom extensionality,
predicate mem = mem, lemma extensionality,
constant empty = empty, lemma empty_def,
function add = add, lemma add_def,
function remove = remove, lemma remove_def,
......
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