Commit 418f57db authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

More doc about FromPure.

parent 6a086fc6
...@@ -43,6 +43,19 @@ Proof. by exists φ. Qed. ...@@ -43,6 +43,19 @@ Proof. by exists φ. Qed.
Hint Extern 0 (IntoPureT _ _) => Hint Extern 0 (IntoPureT _ _) =>
notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances. notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
(* [FromPure] is used when introducing a pure assertion. It is used by
iPure, the "[%]" specialization pattern, and the [with "[%]"]
pattern when using [iAssert].
The [a] Boolean asserts whether we introduce the pure assertion in
an affine way or in an absorbing way. When [FromPure true P φ] is
derived, then [FromPure false P φ] can always be derived too. We
use [true] for specialization patterns and [false] for the [iPure]
This Boolean is not needed for [IntoPure], because in the case of
[IntoPure], we can have the same behavior by asking that [P] be
[Affine]. *)
Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) := Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
from_pure : bi_affinely_if a ⌜φ⌝ P. from_pure : bi_affinely_if a ⌜φ⌝ P.
Arguments FromPure {_} _ _%I _%type_scope : simpl never. Arguments FromPure {_} _ _%I _%type_scope : simpl never.
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