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
Rodolphe Lepigre
Iris
Commits
a0b4ccc2
Commit
a0b4ccc2
authored
Aug 30, 2019
by
Dan Frumin
Browse files
fix typo
parent
eaeb5851
Changes
1
Hide whitespace changes
Inline
Side-by-side
docs/paradoxes.tex
View file @
a0b4ccc2
...
...
@@ -79,7 +79,7 @@ With this lemma in hand, the proof of \thmref{thm:counterexample-1} is simple.
\label
{
app:section:invariants-without-a-later
}
Now we come to the main paradox: if we remove the
$
\later
$
from
\ruleref
{
inv-open
}
, the logic becomes inconsistent.
The theorem is stated as general as possible so t
a
ht it also applies to previous, less powerful versions of Iris.
The theorem is stated as general as possible so th
a
t it also applies to previous, less powerful versions of Iris.
\begin{thm}
\label
{
thm:counterexample-2
}
...
...
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