Skip to content
Snippets Groups Projects
Commit 0c6202e4 authored by Cécile Ruet-Cros's avatar Cécile Ruet-Cros
Browse files

[wp] vset: clean useless lemmas in test

parent f5a61bd8
No related branches found
No related tags found
No related merge requests found
......@@ -53,18 +53,6 @@ theory Vset
axiom member_bool : forall x:'a. forall s:set 'a [member_bool x s].
if mem x s then member_bool x s = True else member_bool x s = False
lemma member_range : forall x:int,a:int,b:int [mem x (range a b)].
mem x (range a b) <-> (a <= x /\ x <= b)
lemma member_range_sup : forall x:int,a:int [mem x (range_sup a)].
mem x (range_sup a) <-> (a <= x)
lemma member_range_inf : forall x:int,b:int [mem x (range_inf b)].
mem x (range_inf b) <-> (x <= b)
lemma member_range_all : forall x:int [mem x range_all].
mem x range_all
(* -------------------------------------------------------------------------- *)
end
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment