Finite.v 345 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
From Coq Require Import List.
Import ListNotations.

Class Finite (T : Type) :=
  build_finite {
    elements : list T;
    elements_set : NoDup elements;
    elements_all : forall (t : T), In t elements;
  }.

Arguments elements _ {_}.
Arguments elements_set _ {_}.
Arguments elements_all _ {_}.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
15
Hint Resolve elements_set elements_all : core.