Commit 2383b600 authored by Robbert Krebbers's avatar Robbert Krebbers

Instance for `Timeless (□ P)`.

parent 1fc708f1
......@@ -449,6 +449,10 @@ Proof. rewrite /bi_affinely; apply _. Qed.
Global Instance absorbingly_timeless P : Timeless P Timeless (<absorb> P).
Proof. rewrite /bi_absorbingly; apply _. Qed.
Global Instance intuitionistically_timeless P :
Timeless (PROP:=PROP) emp Timeless P Timeless ( P).
Proof. rewrite /bi_intuitionistically; apply _. Qed.
Global Instance eq_timeless {A : ofeT} (a b : A) :
Discrete a Timeless (PROP:=PROP) (a b).
Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
......
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