Skip to content
Snippets Groups Projects
Commit c25d0657 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Test.

parent ab1c4c33
No related branches found
No related tags found
1 merge request!429Make sure that `naive_solver` does not create any new evars on leafs.
From stdpp Require Import sets.
From stdpp Require Import sets gmap.
Lemma foo `{Set_ A C} (x : A) (X Y : C) : x X Y x X.
Proof. intros Hx. set_unfold in Hx. tauto. Qed.
......@@ -7,3 +7,7 @@ Proof. intros Hx. set_unfold in Hx. tauto. Qed.
Lemma elem_of_list_bind_again {A B} (x : B) (l : list A) f :
x l ≫= f y, x f y y l.
Proof. set_solver. Qed.
(** Should not leave any evars, see issue #163 *)
Goal {[0]} dom ( : gmap nat nat) ∅.
Proof. set_solver. Qed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment