Commit f5141d1d authored by Robbert Krebbers's avatar Robbert Krebbers

Add `FromForall` instance for `not`. This fixes issue #108.

parent 441894ae
......@@ -772,6 +772,9 @@ Proof. done. Qed.
Global Instance from_forall_pure {A} (φ : A Prop) :
@FromForall M A ( a : A, φ a) (λ a, φ a )%I.
Proof. by rewrite /FromForall pure_forall. Qed.
Global Instance from_forall_pure_not (φ : Prop) :
@FromForall M φ (¬ φ⌝) (λ a : φ, False)%I.
Proof. by rewrite /FromForall pure_forall. Qed.
Global Instance from_forall_impl_pure P Q φ :
IntoPureT P φ FromForall (P Q) (λ _ : φ, Q)%I.
Proof.
......
......@@ -233,6 +233,9 @@ Qed.
Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
x1 = x2 ( x2 = x3 x3 x4 P) - x1 = x4 P.
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
Lemma test_iItros_pure : ( ¬False : uPred M)%I.
Proof. by iIntros (?). Qed.
End tests.
Section more_tests.
......
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