Fix typo

parent 6b6c6b63
...@@ -11,7 +11,7 @@ Set Primitive Projections. ...@@ -11,7 +11,7 @@ Set Primitive Projections.
cases, we do not even need non-expansiveness. cases, we do not even need non-expansiveness.
*) *)
(** Unbundeled version *) (** Unbundled version *)
Class Dist A := dist : nat relation A. Class Dist A := dist : nat relation A.
Instance: Params (@dist) 3 := {}. Instance: Params (@dist) 3 := {}.
Notation "x ≡{ n }≡ y" := (dist n x y) Notation "x ≡{ n }≡ y" := (dist n x y)
...@@ -43,7 +43,7 @@ Record OfeMixin A `{Equiv A, Dist A} := { ...@@ -43,7 +43,7 @@ Record OfeMixin A `{Equiv A, Dist A} := {
mixin_dist_S n x y : x {S n} y x {n} y mixin_dist_S n x y : x {S n} y x {n} y
}. }.
(** Bundeled version *) (** Bundled version *)
Structure ofeT := OfeT { Structure ofeT := OfeT {
ofe_car :> Type; ofe_car :> Type;
ofe_equiv : Equiv ofe_car; ofe_equiv : Equiv ofe_car;
......
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