Commit 0b908b36 authored by Robbert Krebbers's avatar Robbert Krebbers

Some missing unicode arrows.

parent dc9135cb
Pipeline #4105 failed with stage
......@@ -94,19 +94,19 @@ Global Instance from_pure_bupd P φ : FromPure P φ → FromPure (|==> P) φ.
Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1 P2) (φ1 φ2).
FromPure P1 φ1 FromPure P2 φ2 FromPure (P1 P2) (φ1 φ2).
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1 P2) (φ1 φ2).
FromPure P1 φ1 FromPure P2 φ2 FromPure (P1 P2) (φ1 φ2).
Proof. rewrite /FromPure pure_and always_and_sep_l. by intros -> ->. Qed.
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1 P2) (φ1 φ2).
FromPure P1 φ1 FromPure P2 φ2 FromPure (P1 P2) (φ1 φ2).
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1 P2) (φ1 φ2).
IntoPure P1 φ1 FromPure P2 φ2 FromPure (P1 P2) (φ1 φ2).
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1 - P2) (φ1 φ2).
IntoPure P1 φ1 FromPure P2 φ2 FromPure (P1 - P2) (φ1 φ2).
Proof.
rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
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