我想在 Coq/SSReflect 中创建一个归纳定义的枚举类型，例如
Inductive E: Type := A | B | C.
因为finType它显然是有限类型。我有三个解决方案来做到这一点，但所有的解决方案都比我预期的要复杂，而且永远不会令人满意。
在第一个解决方案中，我为eqType、choiceType和实现了 mixin countType。finType
Require Import all_ssreflect.
Inductive E := A | B | C.
Definition E_to_ord (e:E) : 'I_3.
by apply Ordinal with (match e with A => 0 | B => 1 | C => 2 end); case e.
Defined.
Definition E_of_ord (i:'I_3) : E.
by case i=>m ltm3; apply(match m with 0 => A | 1 => …