From 91a46cc0a4d989f667f1d27cd19d02e280680f20 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 17 Feb 2019 21:30:55 +0100
Subject: [PATCH] explain NoDup_enum

---
 theories/finite.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/finite.v b/theories/finite.v
index c5013d76..c81b8446 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -5,6 +5,7 @@ Set Default Proof Using "Type".
 
 Class Finite A `{EqDecision A} := {
   enum : list A;
+  (* [NoDup] makes it easy to define the cardinality of the type. *)
   NoDup_enum : NoDup enum;
   elem_of_enum x : x ∈ enum
 }.
-- 
GitLab