假设如下:
Variable A : finType.
Variable B : finType.
Variable C : finType.
并且一个被定义为:
Record example := Example {
example_A : A;
example_B : B;
example_C : C;
}.
直觉上,似乎这个例子也必须是finType
。
从其他代码库来看,我发现人们使用以下形式的构造方式,针对只有一个非证明项的记录派生finType
。
Definition <record>_subType := Eval hnf in [subtype for <record-accessor>].
Definition <record>_finMixin := Eval hnf in [finMixin of <record> by <:].
但在这种情况下,记录中有多个字段。
是否有自动方式可以为记录派生fintype?如果没有,如何为记录派生fintype?