I have a type `foo`

:

```
Inductive foo: Type :=
| Foo0 | Foo1 | Foo2.
```

How can I 'declare' it to be a `finType`

?

I guess I need to use `isFinite.Build`

for this.

But how can it be done?

```
HB.about finType.
(*
HB: isFinite.Build is a factory constructor (from "./fintype.v", line 161)
HB: isFinite.Build requires its subject to be already equipped with:
- hasDecEq
HB: isFinite.Build provides the following mixins:
- isFinite
HB: arguments: isFinite.Build T [enum_subdef] enumP_subdef
- T : Type
- enum_subdef : seq T
- enumP_subdef :
Finite.axiom
(T:={|
Equality.sort := T;
Equality.class :=
{| Equality.eqtype_hasDecEq_mixin := Finite.class T |}
|}) enum_subdef
*)
```

I suppose this means, I need to produce a `enum_subdef`

and `enumP_subdef`

.

I think I get how `enum_subdef`

should be like: `[Foo0; Foo1; Foo2]`

But how should `enumP_subdef`

be? Does it mean, I first need to make

`foo`

an `eqtype`

?

Yes. Alternatively, you can also "copy" the finType structure of another type if you have an injective function to it, see can_type and pcan_type in https://github.com/math-comp/math-comp/blob/1a09520497a1bac2fd2f12778ed1dba119407c91/mathcomp/ssreflect/choice.v#L46 , the code will be something like `Finite.copy foo (pcan_type foo_natK)`

where `foo_natK`

will be some proof of cancelation of some ffunctions foo -> nat and nat -> foo (for instance).

Given a type `A: finType`

, does it make sense to say that `f: (B: Type) -> A`

is finite?

As in, being able to state that `f`

is also a `finType`

.

You would need for `B`

to be finite and the `functional_extentionality`

axiom (see https://github.com/math-comp/analysis/blob/2a51379c7c7cabe51e2bcf3e0f6b9111fba6e560/classical/boolp.v#L65) to have that `B -> A`

is finite. There is `{ffun _ -> _}`

from https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/finfun.v that might do what you want.

Last updated: Jul 25 2024 at 15:02 UTC