Commit 6db3649f authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Ralf Jung
Browse files

improve comments

parent ce6f4e19
......@@ -104,8 +104,8 @@ Section bi_mixin.
(* The laws of a "frame" (https://ncatlab.org/nlab/show/frame, not to be
confused with separation logic terminology): commuting with finite
conjunction and infinite disjunction.
The null-ary case, [True ⊢ <pers> True], is derivable from the other laws
([persistently_True]). *)
The null-ary case, [persistently_True : True ⊢ <pers> True], is derivable from the
other laws. *)
bi_mixin_persistently_and_2 (P Q : PROP) :
((<pers> P) (<pers> Q)) <pers> (P Q);
bi_mixin_persistently_exist_1 {A} (Ψ : A PROP) :
......
......@@ -25,7 +25,7 @@ Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
(* The following law and [persistently_impl_plainly] below are very similar,
and indeed they hold not just for persistently and plainly, but for any
modality defined as `M P n x := ∀ y, R x y → P n y`. *)
modality defined as [M P n x := ∀ y, R x y → P n y]. *)
bi_plainly_mixin_plainly_impl_plainly (P Q : PROP) :
( P Q) ( P Q);
......
Supports Markdown
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