Commit daf6f5e8 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'ralf/propofe' into 'master'

add OFE structure for Prop

See merge request iris/iris!418
parents acea2a52 88efaeeb
......@@ -946,12 +946,19 @@ Notation discrete_ofe_equivalence_of A := ltac:(
Instance leibnizO_leibniz A : LeibnizEquiv (leibnizO A).
Proof. by intros x y. Qed.
(** * Basic Coq types *)
Canonical Structure boolO := leibnizO bool.
Canonical Structure natO := leibnizO nat.
Canonical Structure positiveO := leibnizO positive.
Canonical Structure NO := leibnizO N.
Canonical Structure ZO := leibnizO Z.
Section prop.
Instance Prop_equiv : Equiv Prop := iff.
Instance Prop_equivalence : Equivalence (@{PROP}) := _.
Canonical Structure PropO := discreteO Prop.
End prop.
(** * Option type *)
Section option.
Context {A : ofeT}.
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