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

Stylistic tweaks in `monPred`.

parent 88aa1108
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 6 deletions
theories/bi/monpred.v
+ 3
− 6
View file @ 6231b7b9
...@@ -447,13 +447,10 @@ Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed. ...@@ -447,13 +447,10 @@ Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
Global Instance monPred_at_affine P i : Affine P → Affine (P i). Global Instance monPred_at_affine P i : Affine P → Affine (P i).
Proof. move => [] /(_ i). unfold Affine. by unseal. Qed. Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
(* Note that monPred_in is *not* Plain, because it does depend on the (** Note that [monPred_in] is *not* [Plain], because it depends on the index. *)
index. *) Global Instance monPred_in_persistent i : Persistent (@monPred_in I PROP i).
Global Instance monPred_in_persistent i :
Persistent (@monPred_in I PROP i).
Proof. unfold Persistent. unseal; split => ?. by apply bi.pure_persistent. Qed. Proof. unfold Persistent. unseal; split => ?. by apply bi.pure_persistent. Qed.
Global Instance monPred_in_absorbing i : Global Instance monPred_in_absorbing i : Absorbing (@monPred_in I PROP i).
Absorbing (@monPred_in I PROP i).
Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed. Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed.
Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed. Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
......
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