diff --git a/theories/infinite.v b/theories/infinite.v index fe5759237f57c162f509f86e06c1cb4bdb51833b..3480c9f704b1a35f60c54e7bf5ce31985348b5e0 100644 --- a/theories/infinite.v +++ b/theories/infinite.v @@ -6,9 +6,10 @@ From stdpp Require Import pretty relations. (** 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 }. +Class Infinite A := { + inject: nat → A; + inject_injective :> Inj (=) (=) inject; +}. Instance string_infinite: Infinite string := {| inject := λ x, "~" +:+ pretty x |}. Instance nat_infinite: Infinite nat := {| inject := id |}.