Commit b600a5bb authored by Ralf Jung's avatar Ralf Jung
Browse files

test bi Lemma scopes

parent fc8e7e87
......@@ -7,3 +7,10 @@ Proof. apply _. Qed.
Lemma test_impl_persistent_2 `{!BiPlainly PROP} :
Persistent (PROP:=PROP) (True True True).
Proof. apply _. Qed.
(* Test that the right scopes are used. *)
Lemma test_bi_scope {PROP : bi} : True.
Proof.
(* [<affine> True] is implicitly in %I scope. *)
pose proof (bi.wand_iff_refl (PROP:=PROP) (<affine> True)).
Abort.
Supports Markdown
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