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

Apply 2 suggestion(s) to 1 file(s)

parent c5d09720
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
iris/bi/lib/fixpoint.v
+ 2
− 2
View file @ 2056ec6f
...@@ -104,7 +104,7 @@ Section least. ...@@ -104,7 +104,7 @@ Section least.
revert x. iApply least_fixpoint_iter; first solve_proper. revert x. iApply least_fixpoint_iter; first solve_proper.
iIntros "!> %y #HF !>". iApply least_fixpoint_unfold. iIntros "!> %y #HF !>". iApply least_fixpoint_unfold.
iApply (bi_mono_pred with "[] HF"); first solve_proper. iApply (bi_mono_pred with "[] HF"); first solve_proper.
by iIntros "!# %x #?". by iIntros "!> %x #?".
Qed. Qed.
Lemma least_fixpoint_persistent_absorbing : Lemma least_fixpoint_persistent_absorbing :
...@@ -116,7 +116,7 @@ Section least. ...@@ -116,7 +116,7 @@ Section least.
iApply least_fixpoint_iter; first solve_proper. iApply least_fixpoint_iter; first solve_proper.
iIntros "!> %y #HF !>". rewrite least_fixpoint_unfold. iIntros "!> %y #HF !>". rewrite least_fixpoint_unfold.
iApply (bi_mono_pred with "[] HF"); first solve_proper. iApply (bi_mono_pred with "[] HF"); first solve_proper.
by iIntros "!# %x #?". by iIntros "!> %x #?".
Qed. Qed.
End least. End least.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment