NonEmptyFintype.v

From mathcomp Require Export fintype.

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

Module NonEmptyFintype.

  Section Def.

    Variable T : finType.

    Record mixin_of := Mixin {
      default : T;
    }.
    Structure class_of (T : finType):= Class {
      base : Finite.class_of T;
      mixin : mixin_of
    }.
    Structure type := Pack {
      sort : finType ;
      class_ : class_of sort
    }.

  End Def.

  Section NonEmptyFintype_of.

    Variable T : finType.
    Variable x : T.

    Definition nonEmptyFinType_of : type T :=
      {|
        sort := T;
        class_ := {|
          base := Finite.class T;
          mixin := {| default := x |}
        |};
      |}.

  End NonEmptyFintype_of.


Module Exports.
  Coercion base : class_of >-> Finite.class_of.
  Coercion sort : type >-> finType.
  Notation nonEmptyFintype := NonEmptyFintype.type.
  Notation default T := (default (mixin (class_ T))).
  Notation nonEmptyFinType_of := NonEmptyFintype.nonEmptyFinType_of.

  End Exports.

End NonEmptyFintype.

Export NonEmptyFintype.Exports.