Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Pierre-Marie Pédrot
Iris
Commits
77695c5f
Commit
77695c5f
authored
Jan 23, 2019
by
Mackie Loeffel
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Added note about unicode asterisk to docs
parent
9d39a93e
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
4 additions
and
2 deletions
+4
-2
ProofMode.md
ProofMode.md
+4
-2
No files found.
ProofMode.md
View file @
77695c5f
...
...
@@ -101,7 +101,8 @@ Separation logic-specific tactics
+
`%`
: repeatedly frame hypotheses from the Coq context.
+
`#`
: repeatedly frame hypotheses from the intuitionistic context.
+
`∗`
: frame as much of the spatial context as possible.
+
`∗`
: frame as much of the spatial context as possible. (N.B: this
is the unicode symbol
`∗`
, not the regular asterisk
`*`
.)
Notice that framing spatial hypotheses makes them disappear, but framing Coq
or intuitionistic hypotheses does not make them disappear.
...
...
@@ -189,7 +190,8 @@ following _selection patterns_:
-
`H`
: select the hypothesis named
`H`
.
-
`%`
: select the entire pure/Coq context.
-
`#`
: select the entire intuitionistic context.
-
`∗`
: select the entire spatial context.
-
`∗`
: select the entire spatial context. (N.B: this
is the unicode symbol
`∗`
, not the regular asterisk
`*`
.)
Introduction patterns
=====================
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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