Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Issues
#157
Closed
Open
Issue created
Feb 20, 2018
by
Robbert Krebbers
@robbertkrebbers
Maintainer
`done` loops in proofmode
Lemma
test
:
∃
R
,
R
⊢
∀
P
,
P
.
Proof
.
eexists
.
iIntros
"?"
(
P
).
done
.