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

Fix naming inconsistencies in `ofe_iso`.

parent 52bfb792
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 3 deletions
theories/algebra/ofe.v
+ 3
− 3
View file @ 0e2975ec
...@@ -1591,11 +1591,11 @@ Section ofe_iso. ...@@ -1591,11 +1591,11 @@ Section ofe_iso.
Global Instance ofe_iso_2_ne : NonExpansive (ofe_iso_2 (A:=A) (B:=B)). Global Instance ofe_iso_2_ne : NonExpansive (ofe_iso_2 (A:=A) (B:=B)).
Proof. by destruct 1. Qed. Proof. by destruct 1. Qed.
Lemma iso_ofe_ofe_mixin : OfeMixin (ofe_iso A B). Lemma ofe_iso_ofe_mixin : OfeMixin (ofe_iso A B).
Proof. by apply (iso_ofe_mixin (λ I, (ofe_iso_1 I, ofe_iso_2 I))). Qed. Proof. by apply (iso_ofe_mixin (λ I, (ofe_iso_1 I, ofe_iso_2 I))). Qed.
Canonical Structure ofe_isoO : ofeT := OfeT (ofe_iso A B) iso_ofe_ofe_mixin. Canonical Structure ofe_isoO : ofeT := OfeT (ofe_iso A B) ofe_iso_ofe_mixin.
Global Instance iso_ofe_cofe `{!Cofe A, !Cofe B} : Cofe ofe_isoO. Global Instance ofe_iso_cofe `{!Cofe A, !Cofe B} : Cofe ofe_isoO.
Proof. Proof.
apply (iso_cofe_subtype' apply (iso_cofe_subtype'
(λ I : prodO (A -n> B) (B -n> A), (λ I : prodO (A -n> B) (B -n> A),
......
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