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

More sensible instance names for `monPred`'s `BiAffine` and `BiPositive`.

parent 89a00a27
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
theories/bi/monpred.v
+ 2
− 2
View file @ 88aa1108
......@@ -435,9 +435,9 @@ Proof. unseal. split. solve_proper. Qed.
Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
Proof. solve_proper. Qed.
Global Instance monPred_positive : BiPositive PROP → BiPositive monPredI.
Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
Proof. split => ?. unseal. apply bi_positive. Qed.
Global Instance monPred_affine : BiAffine PROP → BiAffine monPredI.
Global Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI.
Proof. split => ?. unseal. by apply affine. Qed.
Global Instance monPred_at_persistent P i : Persistent P → Persistent (P i).
......
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