Skip to content

GitLab

Commit 81ba0b8b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

False is affine.

parent fa43edc5
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 0 deletions
theories/bi/derived_laws_bi.v
View file @ 81ba0b8b
......@@ -1274,6 +1274,8 @@ End persistent_bi_absorbing.
(* Affine instances *)
Global Instance emp_affine_l : Affine (PROP:=PROP) emp.
Proof. by rewrite /Affine. Qed.
Global Instance False_affine : Affine (PROP:=PROP) False.
Proof. by rewrite /Affine False_elim. Qed.
Global Instance and_affine_l P Q : Affine P → Affine (P ∧ Q).
Proof. rewrite /Affine=> ->; auto. Qed.
Global Instance and_affine_r P Q : Affine Q → Affine (P ∧ Q).
......
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