Documentation

LeanPool.LanguageGeneration.FiniteWitness

A complete finite-witness characterization of ordinary generation #

The public entry points are GenLimit.FiniteWitness.ordinary_iff_finiteWitnesses, GenLimit.FiniteWitness.full_characterization, and GenLimit.FiniteWitness.universal_normalization.

All ordinary-generation definitions come from the upstream generic Core API.