Skip to content

Add support for auto-generating Inductives for enums

Lennard Gäher requested to merge ci/generate-enum into main

Enums which are not annotated with a refined_by attribute get an auto-generated Coq Inductive they are refined by. Also start refactoring the whole Coq pretty printing business.

Merge request reports