Skip to content

Provide an Infinite typeclass and a generic implementation of Fresh.

Ghost User requested to merge archived_projects/coq-stdpp:freshstring into master

This provides a generic implementation of Fresh for infinite types.

In detail, it adds:

  • An Infinite type class. A type T is infinite if there is an injection from nat to T.
  • A generic implementation of Fresh A C for an infinite type A and a finite collection type C, by way of linear search for a fresh element.
  • Instances of Infinite for a handful of types, including positive/natural/integer types and string.
  • A generic Fresh for finite collections of strings. As an implementation detail, the generated strings are all of the form "~n" for some natural number n.
  • Some minor additions (pretty-printer for nat, Fix unfolding lemma for setoids).

Merge request reports