Skip to content
Snippets Groups Projects
Commit 3ef1bbb5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Stronger `IntoWand` instance for the □ modality.

parent 245e1d08
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/class_instances_bi.v
+ 2
− 2
View file @ 3ef1bbb5
......@@ -419,8 +419,8 @@ Proof.
Qed.
Global Instance into_wand_intuitionistically p q R P Q :
IntoWand p q R P Q → IntoWand p q (□ R) P Q.
Proof. by rewrite /IntoWand intuitionistically_elim. Qed.
IntoWand true q R P Q → IntoWand p q (□ R) P Q.
Proof. rewrite /IntoWand /= => ->. by rewrite {1}intuitionistically_if_elim. Qed.
Global Instance into_wand_persistently_true q R P Q :
IntoWand true q R P Q → IntoWand true q (<pers> R) P Q.
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
......
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