Skip to content
Snippets Groups Projects
Commit 62573506 authored by Simcha van Collem's avatar Simcha van Collem
Browse files

Add fixme about least_fixpoint_persistent lemmas

parent 2413607e
No related branches found
No related tags found
No related merge requests found
Pipeline #74328 passed
......@@ -154,6 +154,8 @@ Section general.
x y, Affine (bi_rtc R x y).
Proof. intros. apply least_fixpoint_affine; apply _. Qed.
(* FIXME: It would be nicer to use the least_fixpoint_persistent lemmas,
but they seem to weak. *)
Global Instance bi_rtc_persistent :
( x y, Persistent (R x y))
x y, Persistent (bi_rtc R x y).
......@@ -263,6 +265,8 @@ Section general.
x y, Absorbing (bi_tc R x y).
Proof. intros. apply least_fixpoint_absorbing; apply _. Qed.
(* FIXME: It would be nicer to use the least_fixpoint_persistent lemmas,
but they seem to weak. *)
Global Instance bi_tc_persistent :
( x y, Persistent (R x y))
x y, Persistent (bi_tc R x y).
......
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