Skip to content
Snippets Groups Projects
Commit e1eaa456 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'fix-typo' into 'master'

Fix typo

See merge request iris/iris!687
parents 96191ed7 b5960731
No related branches found
No related tags found
1 merge request!687Fix typo
Pipeline #47250 passed
......@@ -247,7 +247,7 @@ Global Hint Mode IsExcept0 + ! : typeclass_instances.
The inputs are [p], [P] and [Q], and the outputs are [φ], [p'], [P'] and [Q'].
The class is used to transform a hypothesis [P] into a hypothesis [P'], given
a goal [Q], which is simultaniously transformed into [Q']. The Booleans [p]
a goal [Q], which is simultaneously transformed into [Q']. The Booleans [p]
and [p'] indicate whether the original, respectively, updated hypothesis reside
in the persistent context (iff [true]). The proposition [φ] can be used to
express a side-condition that [iMod] will generate (if not [True]).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment