Commit ae0b5798 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Break some very long lines in `class_instances_bi`.

parent 7a4ff479
...@@ -698,7 +698,8 @@ Qed. ...@@ -698,7 +698,8 @@ Qed.
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P Q) P Q. Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P Q) P Q.
Proof. Proof.
rewrite /IntoAnd /= intuitionistically_sep -and_sep_intuitionistically intuitionistically_and //. rewrite /IntoAnd /= intuitionistically_sep
-and_sep_intuitionistically intuitionistically_and //.
Qed. Qed.
Global Instance into_and_sep_affine P Q : Global Instance into_and_sep_affine P Q :
TCOr (Affine P) (Absorbing Q) TCOr (Absorbing P) (Affine Q) TCOr (Affine P) (Absorbing Q) TCOr (Absorbing P) (Affine Q)
...@@ -990,7 +991,9 @@ Global Instance into_forall_wand P Q : ...@@ -990,7 +991,9 @@ Global Instance into_forall_wand P Q :
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed. Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed.
Global Instance into_forall_impl `{!BiAffine PROP} P Q : Global Instance into_forall_impl `{!BiAffine PROP} P Q :
IntoForall (P Q) (λ _ : P, Q) | 10. IntoForall (P Q) (λ _ : P, Q) | 10.
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl //. Qed. Proof.
rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl //.
Qed.
(** FromForall *) (** FromForall *)
Global Instance from_forall_forall {A} (Φ : A PROP) : Global Instance from_forall_forall {A} (Φ : A PROP) :
......
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