Commit 86bc5be1 authored by Ralf Jung's avatar Ralf Jung

remark on AlwaysStable assertions

parent 732b3d49
......@@ -301,6 +301,8 @@ Infix "↔" := uPred_iff : uPred_scope.
Class TimelessP {M} (P : uPred M) := timelessP : P (P False).
Arguments timelessP {_} _ {_}.
(* TODO: Derek suggested to call such assertions "persistent", which we now
do in the paper. *)
Class AlwaysStable {M} (P : uPred M) := always_stable : P P.
Arguments always_stable {_} _ {_}.
......
Markdown is supported
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