From Undecidability.Shared.Libs.PSL Require Export EqDecDef.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Records.
Unset Printing Implicit Defensive.

Fixpoint count (X: Type) `{eq_dec X} (A: list X) (x: X) {struct A} : nat :=
  match A with
  | nil => O
  | cons y A' => if Dec (x=y) then S(count A' x) else count A' x end.


Class finTypeC (type:eqType) : Type :=
  FinTypeC {
      enum: list type;
      enum_ok: forall x: type, count enum x = 1
  }.

Structure finType : Type :=
  FinType
    {
      type:> eqType;
      class: finTypeC type
    }.

Arguments FinType type {class}.
#[global]
Existing Instance class | 0.

#[export] Hint Extern 5 (finTypeC (EqType ?x)) => unfold x : typeclass_instances.

Canonical Structure finType_CS (X : Type) {p : eq_dec X} {class : finTypeC (EqType X)} : finType := FinType (EqType X).

Arguments finType_CS (X) {_ _}.