From 8389dcbf0fb39d0655ccf5d0fb5ba0380bd55f07 Mon Sep 17 00:00:00 2001
From: Johannes Kloos <jkloos@mpi-sws.org>
Date: Tue, 31 Oct 2017 11:35:54 +0100
Subject: [PATCH] Provide a type class for infinite types.

Infinity is described by having an injection from nat.
---
 theories/base.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 6f02d571..933535d5 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1125,6 +1125,13 @@ Class FreshSpec A C `{ElemOf A C,
   is_fresh (X : C) : fresh X ∉ X
 }.
 
+(** The class [Infinite] axiomatizes types with infinitely many elements
+by giving an injection from the natural numbers into the type. It is mostly
+used to provide a generic [fresh] algorithm. *)
+Class Infinite A :=
+  { inject: nat → A;
+    inject_injective:> Inj (=) (=) inject }.
+
 (** * Miscellaneous *)
 Class Half A := half: A → A.
 Hint Mode Half ! : typeclass_instances.
-- 
GitLab