Commit b9d25e99 authored by Tej Chajed's avatar Tej Chajed Committed by Ralf Jung
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent 6d1a88a5
......@@ -251,7 +251,7 @@ Lemma test_iDestruct_exists_automatic_def P :
an_exists P - k, ^k P.
Proof. iDestruct 1 as (?) "H". by iExists an_exists_name. Qed.
(* use an Iris intro pattern [% H] to indicate iExistDestruct rather than (?) *)
(* use an Iris intro pattern [% H] rather than (?) to indicate iExistDestruct *)
Lemma test_exists_intro_pattern_anonymous P (Φ: nat PROP) :
P ( y:nat, Φ y) - x, P Φ x.
Proof.
......
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