diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finfun.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/generic_quotient.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 12 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 18 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnotations.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 2 |
14 files changed, 41 insertions, 41 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 6d18825..698f2e7 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -5,12 +5,12 @@ From mathcomp Require Import div fintype tuple finfun. (******************************************************************************) (* This file provides a generic definition for iterating an operator over a *) -(* set of indices (bigop); this big operator is parametrized by the return *) +(* set of indices (bigop); this big operator is parameterized by the return *) (* type (R), the type of indices (I), the operator (op), the default value on *) (* empty lists (idx), the range of indices (r), the filter applied on this *) (* range (P) and the expression we are iterating (F). The definition is not *) (* to be used directly, but via the wide range of notations provided and *) -(* and which support a natural use of big operators. *) +(* which support a natural use of big operators. *) (* To improve performance of the Coq typechecker on large expressions, the *) (* bigop constant is OPAQUE. It can however be unlocked to reveal the *) (* transparent constant reducebig, to let Coq expand summation on an explicit *) @@ -27,7 +27,7 @@ From mathcomp Require Import div fintype tuple finfun. (* 2. Results depending on the properties of the operator: *) (* We distinguish: monoid laws (op is associative, idx is an identity *) (* element), abelian monoid laws (op is also commutative), and laws with *) -(* a distributive operation (semi-rings). Examples of such results are *) +(* a distributive operation (semirings). Examples of such results are *) (* splitting, permuting, and exchanging bigops. *) (* A special section is dedicated to big operators on natural numbers. *) (******************************************************************************) diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 3a484a1..2af7953 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -5,7 +5,7 @@ From mathcomp Require Import div fintype tuple finfun bigop prime finset. (******************************************************************************) (* This files contains the definition of: *) -(* 'C(n, m) == the binomial coeficient n choose m. *) +(* 'C(n, m) == the binomial coefficient n choose m. *) (* n ^_ m == the falling (or lower) factorial of n with m terms, i.e., *) (* the product n * (n - 1) * ... * (n - m + 1). *) (* Note that n ^_ m = 0 if m > n, and 'C(n, m) = n ^_ m %/ m/!. *) diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index f5d95e8..296f85e 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -38,7 +38,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* x != y :> T <=> x and y compare unequal at type T. *) (* x =P y :: a proof of reflect (x = y) (x == y); x =P y coerces *) (* to x == y -> x = y. *) -(* eq_op == the boolean relation behing the == notation. *) +(* eq_op == the boolean relation behind the == notation. *) (* pred1 a == the singleton predicate [pred x | x == a]. *) (* pred2, pred3, pred4 == pair, triple, quad predicates. *) (* predC1 a == [pred x | x != a]. *) @@ -73,7 +73,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* insub x = Some u with val u = x if P x, *) (* None if ~~ P x *) (* The insubP lemma encapsulates this dichotomy. *) -(* P should be infered from the expected return type. *) +(* P should be inferred from the expected return type. *) (* innew x == total (non-option) variant of insub when P = predT. *) (* {? x | P} == option {x | P} (syntax for casting insub x). *) (* insubd u0 x == the generic projection with default value u0. *) @@ -92,7 +92,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* [subType for S_val by Srect], [newType for S_val by Srect] *) (* variants of the above where the eliminator is explicitly provided. *) (* Here S no longer needs to be syntactically identical to {x | P x} or *) -(* wrapped T, but it must have a derived constructor S_Sub statisfying an *) +(* wrapped T, but it must have a derived constructor S_Sub satisfying an *) (* eliminator Srect identical to the one the Coq Inductive command would *) (* have generated, and S_val (S_Sub x Px) (resp. S_val (S_sub x) for the *) (* newType form) must be convertible to x. *) diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 749f5e2..0218f6a 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -39,7 +39,7 @@ From mathcomp Require Import fintype tuple. (* limitations referred to above. *) (* ffun0 aT0 == the trivial finfun, from a proof aT0 that #|aT| = 0. *) (* f \in family F == f belongs to the family F (f x \in F x for all x) *) -(* There are addidional operations for non-dependent finite functions, *) +(* There are additional operations for non-dependent finite functions, *) (* i.e., f in {ffun aT -> rT}. *) (* [ffun x => E] := finfun (fun x => E). *) (* The type of E must not depend on x; this restriction *) @@ -155,7 +155,7 @@ Proof. by fix IHt 2 => n [st]; apply/Kstep=> i; apply: IHt. Defined. Set Elimination Schemes. (* End example. *) *) -(* The correspondance between finfun_of and CiC dependent functions. *) +(* The correspondence between finfun_of and CiC dependent functions. *) Section DepPlainTheory. Variables (aT : finType) (rT : aT -> Type). Notation fT := {ffun finPi aT rT}. diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index afd43df..09ca95f 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -776,7 +776,7 @@ Qed. (* has to apply it to the natural numbers corresponding to the line, e.g. *) (* `orbitPcycle 0 2 : fcycle f (orbit x) <-> exists k, iter k.+1 f x = x`. *) (* examples of this are in order_id_cycle and fconnnect_f. *) -(* One may also use lemma all_iffLR to get a one sided impliciation, as in *) +(* One may also use lemma all_iffLR to get a one sided implication, as in *) (* orderPcycle. *) (*****************************************************************************) Lemma orbitPcycle {x} : [<-> diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index cd1a1bb..9953c0d 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -43,7 +43,7 @@ From mathcomp Require Import choice fintype finfun bigop. (* is_transversal X P D <=> X is a transversal of the partition P of D. *) (* transversal P D == a transversal of P, provided P is a partition of D. *) (* transversal_repr x0 X B == a representative of B \in P selected by the *) -(* tranversal X of P, or else x0. *) +(* transversal X of P, or else x0. *) (* powerset A == the set of all subset of the set A. *) (* P ::&: A == those sets in P that are subsets of the set A. *) (* f @^-1: A == the preimage of the collective predicate A under f. *) @@ -56,7 +56,7 @@ From mathcomp Require Import choice fintype finfun bigop. (* [set E | x in A, y in B] == the set of values of E for x drawn from A and *) (* and y drawn from B; B may depend on x. *) (* [set E | x <- A, y <- B & P] == the set of values of E for x drawn from A *) -(* y drawn from B, such that P is trye. *) +(* y drawn from B, such that P is true. *) (* [set E | x : T] == the set of all values of E, with x in type T. *) (* [set E | x : T & P] == the set of values of E for x : T s.t. P is true. *) (* [set E | x : T, y : U in B], [set E | x : T, y : U in B & P], *) @@ -102,7 +102,7 @@ From mathcomp Require Import choice fintype finfun bigop. (* These suffixes are sometimes preceded with an `s' to distinguish them from *) (* their basic ssrbool interpretation, e.g., *) (* card1 : #|pred1 x| = 1 and cards1 : #|[set x]| = 1 *) -(* We also use a trailling `r' to distinguish a right-hand complement from *) +(* We also use a trailing `r' to distinguish a right-hand complement from *) (* commutativity, e.g., *) (* setIC : A :&: B = B :&: A and setICr : A :&: ~: A = set0. *) (******************************************************************************) @@ -146,7 +146,7 @@ Notation "{ 'set' T }" := (set_of (Phant T)) (* preferable to state equalities at the {set _} level, even when comparing *) (* subtype values, because the primitive "injection" tactic tends to diverge *) (* on complex types (e.g., quotient groups). We provide some parse-only *) -(* notation to make this technicality less obstrusive. *) +(* notation to make this technicality less obstructive. *) Notation "A :=: B" := (A = B :> {set _}) (at level 70, no associativity, only parsing) : set_scope. Notation "A :<>: B" := (A <> B :> {set _}) @@ -2128,7 +2128,7 @@ Qed. (**********************************************************************) (* *) -(* Maximum and minimun (sub)set with respect to a given pred *) +(* Maximum and minimum (sub)set with respect to a given pred *) (* *) (**********************************************************************) diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 14d623f..14faf57 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -108,7 +108,7 @@ From mathcomp Require Import path. (* invF inj_f y == the x such that f x = y, for inj_j : injective f with *) (* f : T -> T. *) (* dinjectiveb A f <=> the restriction of f : T -> R to A is injective *) -(* (this is a bolean predicate, R must be an eqType). *) +(* (this is a boolean predicate, R must be an eqType). *) (* injectiveb f <=> f : T -> R is injective (boolean predicate). *) (* pred0b A <=> no x : T satisfies x \in A. *) (* [forall x, P] <=> P (in which x can appear) is true for all values of x *) diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index f572a51..4eeada9 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -10,7 +10,7 @@ From mathcomp Require Import seq fintype. (* provide a helper to quotient T by a decidable equivalence relation (e *) (* : rel T) if T is a choiceType (or encodable as a choiceType modulo e). *) (* *) -(* See "Pragamatic Quotient Types in Coq", proceedings of ITP2013, *) +(* See "Pragmatic Quotient Types in Coq", proceedings of ITP2013, *) (* by Cyril Cohen. *) (* *) (* *** Generic Quotienting *** *) @@ -263,7 +263,7 @@ Hypothesis pi_r : {mono \pi : x y / r x y >-> rq x y}. Hypothesis pi_h : forall (x : T), \pi_qU (h x) = hq (\pi_qT x). Variables (a b : T) (x : equal_to (\pi_qT a)) (y : equal_to (\pi_qT b)). -(* Internal Lemmmas : do not use directly *) +(* Internal Lemmas : do not use directly *) Lemma pi_morph1 : \pi (f a) = fq (equal_val x). Proof. by rewrite !piE. Qed. Lemma pi_morph2 : \pi (g a b) = gq (equal_val x) (equal_val y). Proof. by rewrite !piE. Qed. Lemma pi_mono1 : p a = pq (equal_val x). Proof. by rewrite !piE. Qed. @@ -294,7 +294,7 @@ Notation PiMono2 pi_r := Notation PiMorph11 pi_f := (fun a (x : {pi a}) => EqualTo (pi_morph11 pi_f a x)). -(* lifiting helpers *) +(* lifting helpers *) Notation lift_op1 Q f := (locked (fun x : Q => \pi_Q (f (repr x)) : Q)). Notation lift_op2 Q g := (locked (fun x y : Q => \pi_Q (g (repr x) (repr y)) : Q)). 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. *) (******************************************************************************) diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index bccafa8..9327a2f 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -6,7 +6,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* The basic theory of paths over an eqType; this file is essentially a *) (* complement to seq.v. Paths are non-empty sequences that obey a progression *) (* relation. They are passed around in three parts: the head and tail of the *) -(* sequence, and a proof of (boolean) predicate asserting the progression. *) +(* sequence, and a proof of a (boolean) predicate asserting the progression. *) (* This "exploded" view is rarely embarrassing, as the first two parameters *) (* are usually inferred from the type of the third; on the contrary, it saves *) (* the hassle of constantly constructing and destructing a dependent record. *) @@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* We allow duplicates; uniqueness, if desired (as is the case for several *) (* geometric constructions), must be asserted separately. We do provide *) (* shorthand, but only for cycles, because the equational properties of *) -(* "path" and "uniq" are unfortunately incompatible (esp. wrt "cat"). *) +(* "path" and "uniq" are unfortunately incompatible (esp. wrt "cat"). *) (* We define notations for the common cases of function paths, where the *) (* progress relation is actually a function. In detail: *) (* path e x p == x :: p is an e-path [:: x_0; x_1; ... ; x_n], i.e., we *) @@ -26,7 +26,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* the form [:: f x; f (f x); ...]. This is just a notation *) (* for path (frel f) x p. *) (* sorted e s == s is an e-sorted sequence: either s = [::], or s = x :: p *) -(* is an e-path (this is oten used with e = leq or ltn). *) +(* is an e-path (this is often used with e = leq or ltn). *) (* cycle e c == c is an e-cycle: either c = [::], or c = x :: p with *) (* x :: (rcons p x) an e-path. *) (* fcycle f c == c is an f-cycle, for a function f. *) @@ -47,9 +47,9 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* c (viewed as a cycle), or x if x \notin c. *) (* prev c x == the predecessor of the first occurrence of x in the *) (* sequence c (viewed as a cycle), or x if x \notin c. *) -(* arc c x y == the sub-arc of the sequece c (viewed as a cycle) starting *) +(* arc c x y == the sub-arc of the sequence c (viewed as a cycle) starting *) (* at the first occurrence of x in c, and ending just before *) -(* the next ocurrence of y (in cycle order); arc c x y *) +(* the next occurrence of y (in cycle order); arc c x y *) (* returns an unspecified sub-arc of c if x and y do not both *) (* occur in c. *) (* ucycle e c <-> ucycleb e c (ucycle e c is a Coercion target of type Prop) *) @@ -73,12 +73,12 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* of splitP will also simultaneously replace take (index x p) with p1 and *) (* drop (index x p).+1 p with p2. *) (* - splitPl applies when x \in x0 :: p; it replaces p with p1 ++ p2 and *) -(* simulaneously generates an equation x = last x0 p. *) +(* simultaneously generates an equation x = last x0 p. *) (* - splitPr applies when x \in p; it replaces p with (p1 ++ x :: p2), so x *) (* appears explicitly at the start of the right part. *) (* The parts p1 and p2 are computed using index/take/drop in all cases, but *) -(* only splitP attemps to subsitute the explicit values. The substitution of *) -(* p can be deferred using the dependent equation generation feature of *) +(* only splitP attempts to substitute the explicit values. The substitution *) +(* of p can be deferred using the dependent equation generation feature of *) (* ssreflect, e.g.: case/splitPr def_p: {1}p / x_in_p => [p1 p2] generates *) (* the equation p = p1 ++ p2 instead of performing the substitution outright. *) (* Similarly, eliminating the loop removal lemma shortenP simultaneously *) @@ -86,7 +86,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* last x p'. *) (* Note that although all "path" functions actually operate on the *) (* underlying sequence, we provide a series of lemmas that define their *) -(* interaction with thepath and cycle predicates, e.g., the cat_path equation *) +(* interaction with the path and cycle predicates, e.g., the cat_path equation*) (* can be used to split the path predicate after splitting the underlying *) (* sequence. *) (******************************************************************************) diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index d8f5939..33ea698 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -47,7 +47,7 @@ Unset Printing Implicit Defensive. (* The complexity of any arithmetic operation with the Peano representation *) (* is pretty dreadful, so using algorithms for "harder" problems such as *) -(* factoring, that are geared for efficient artihmetic leads to dismal *) +(* factoring, that are geared for efficient arithmetic leads to dismal *) (* performance -- it takes a significant time, for instance, to compute the *) (* divisors of just a two-digit number. On the other hand, for Peano *) (* integers, prime factoring (and testing) is linear-time with a small *) diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index bccb968..67bc923 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -90,7 +90,7 @@ Require Export Ring. (* V (infix) -- disjunction, as in *) (* leq_eqVlt : (m <= n) = (m == n) || (m < n). *) (* X - exponentiation, as in lognX : logn p (m ^ n) = logn p m * n in *) -(* file prime.v (the suffix is not used in ths file). *) +(* file prime.v (the suffix is not used in the file). *) (* Suffixes that abbreviate operations (D, B, M and X) are used to abbreviate *) (* second-rank operations in equational lemma names that describe left-hand *) (* sides (e.g., mulnDl); they are not used to abbreviate the main operation *) @@ -1531,7 +1531,7 @@ Section NatToNat. Variable (f : nat -> nat). (****************************************************************************) -(* This listing of "Let"s factor out the required premices for the *) +(* This listing of "Let"s factor out the required premises for the *) (* subsequent lemmas, putting them in the context so that "done" solves the *) (* goals quickly *) (****************************************************************************) @@ -1634,7 +1634,7 @@ Module NatTrec. (* Usage: *) (* Import NatTrec. *) -(* in section definining functions, rebinds all *) +(* in section defining functions, rebinds all *) (* non-tail recursive operators. *) (* rewrite !trecE. *) (* in the correctness proof, restores operators *) @@ -1782,7 +1782,7 @@ End NumberInterpretation. (* Num 1 072 399 *) (* to create large numbers for test cases *) (* Eval compute in [Num of some expression] *) -(* to display the resut of an expression that *) +(* to display the result of an expression that *) (* returns a larger integer. *) Record number : Type := Num {bin_of_number :> N}. diff --git a/mathcomp/ssreflect/ssrnotations.v b/mathcomp/ssreflect/ssrnotations.v index dbc7f3d..d85fdf8 100644 --- a/mathcomp/ssreflect/ssrnotations.v +++ b/mathcomp/ssreflect/ssrnotations.v @@ -52,7 +52,7 @@ Reserved Notation "x ^- n" (at level 29, left associativity). Reserved Notation "x *: A" (at level 40). Reserved Notation "A :* x" (at level 40). -(* Reserved notation for set-theretic operations. *) +(* Reserved notation for set-theoretic operations. *) Reserved Notation "A :&: B" (at level 48, left associativity). Reserved Notation "A :|: B" (at level 52, left associativity). Reserved Notation "a |: A" (at level 52, left associativity). diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 10d54f0..ed55b08 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -373,7 +373,7 @@ Variables (n : nat) (T : finType). (* tuple_finMixin could, in principle, be made Canonical to allow for folding *) (* Finite.enum of a finite tuple type (see comments around eqE in eqtype.v), *) (* but in practice it will not work because the mixin_enum projector *) -(* has been burried under an opaque alias, to avoid some performance issues *) +(* has been buried under an opaque alias, to avoid some performance issues *) (* during type inference. *) Definition tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T). Canonical tuple_finType := Eval hnf in FinType (n.-tuple T) tuple_finMixin. |