diff options
Diffstat (limited to 'mathcomp/ssreflect/order.v')
| -rw-r--r-- | mathcomp/ssreflect/order.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 5c8f251..259484a 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -46,7 +46,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* they operate on and then the operands. Here is the exhaustive list of all *) (* such symbols for partial orders and lattices together with their default *) (* display (as displayed by Check). We document their meaning in the *) -(* paragraph adter the next. *) +(* paragraph after the next. *) (* *) (* For porderType T *) (* @Order.le disp T == <=%O (in fun_scope) *) @@ -118,7 +118,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* `Notation "x <<< y" := @Order.lt my_display _ x y (at level ...).` *) (* Non overloaded notations will default to the default display. *) (* *) -(* One may use displays either for convenience or to desambiguate between *) +(* One may use displays either for convenience or to disambiguate between *) (* different structures defined on "copies" of a type (as explained below.) *) (* We provide the following "copies" of types, *) (* the first one is a *documented example* *) @@ -182,7 +182,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* the structures that fits the display one mentioned, but will rather *) (* determine which canonical structure and display to use depending on the *) (* copy of the type one provided. In this sense they are merely displays *) -(* to inform the user of what the inferrence did, rather than additional *) +(* to inform the user of what the inference did, rather than additional *) (* input for the inference. *) (* *) (* Existing displays are either dual_display d (where d is a display), *) @@ -4546,7 +4546,7 @@ Import SubOrder.Exports. (* i.e. without creating a "copy". We use the predefined total_display, which *) (* is designed to parse and print meet and join as minn and maxn. This looks *) (* like standard canonical structure declaration, except we use a display. *) -(* We also use a single factory LeOrderMixin to instanciate three different *) +(* We also use a single factory LeOrderMixin to instantiate three different *) (* canonical declarations porderType, distrLatticeType, orderType *) (* We finish by providing theorems to convert the operations of ordered and *) (* lattice types to their definition without structure abstraction. *) @@ -4692,8 +4692,8 @@ End DvdSyntax. (* we declare it on a "copy" of the type. *) (* We first recover structures that are common to both nat and natdiv *) (* (eqType, choiceType, countType) through the clone mechanisms, then we use *) -(* a single factory MeetJoinMixin to instanciate both porderType and *) -(* distrLatticeType canonical structures,and end with top and bottom. *) +(* a single factory MeetJoinMixin to instantiate both porderType and *) +(* distrLatticeType canonical structures, and end with top and bottom. *) (* We finish by providing theorems to convert the operations of ordered and *) (* lattice types to their definition without structure abstraction. *) (******************************************************************************) |