Commit 861490f0 authored by Ralf Jung's avatar Ralf Jung

FromAffinely instance for intuitionistic modality

parent 373feb82
......@@ -13,6 +13,9 @@ Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
Proof. by rewrite /FromAffinely. Qed.
Global Instance from_affinely_intuitionistically P :
FromAffinely ( P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.
(* IntoAbsorbingly *)
Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
......
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