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
George Pirlea
Iris
Commits
27914f3f
Commit
27914f3f
authored
May 31, 2018
by
Robbert Krebbers
Browse files
Merge branch 'master' into gen_proofmode
parents
07ea98fe
061e8d6a
Changes
2
Hide whitespace changes
Inline
Side-by-side
ProofMode.md
View file @
27914f3f
...
...
@@ -41,7 +41,7 @@ Context management
the resulting goal.
-
`iPoseProof pm_trm as (x1 ... xn) "ipat"`
: put
`pm_trm`
into the context and
eliminates it. This tactic is essentially the same as
`iDestruct`
with the
difference that when
`pm_trm`
is a non-universally quantified
spatial
difference that when
`pm_trm`
is a non-universally quantified
intuitionistic
hypothesis, it will not throw the hypothesis away.
-
`iAssert P with "spat" as "ipat"`
: generates a new subgoal
`P`
and adds the
hypothesis
`P`
to the current goal. The specialization pattern
`spat`
...
...
theories/base_logic/lib/boxes.v
View file @
27914f3f
...
...
@@ -13,7 +13,7 @@ Class boxG Σ :=
Definition
box
Σ
:
gFunctors
:
=
#[
GFunctor
(
authR
(
optionUR
(
exclR
boolC
))
*
optionRF
(
agreeRF
(
▶
∙
))
)
].
Instance
subG_
sts
Σ
Σ
:
subG
box
Σ
Σ
→
boxG
Σ
.
Instance
subG_
box
Σ
Σ
:
subG
box
Σ
Σ
→
boxG
Σ
.
Proof
.
solve_inG
.
Qed
.
Section
box_defs
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment