diff options
Diffstat (limited to 'mathcomp/ssreflect/tuple.v')
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 64585f6..38e3dbe 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -360,7 +360,12 @@ Section UseFinTuple. Variables (n : nat) (T : finType). -Canonical tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T). +(* 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 *) +(* 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. Canonical tuple_subFinType := Eval hnf in [subFinType of n.-tuple T]. |