-
François Bobot authored
encoding_enumeration add projection for enumerated type. Seems to work (on valid and not valid goal) for simplify, spass, eprover see examples/programs/sorted_list.mlw with eprover, spass, simplify!! encoding_enumeration must be used with encoding_decorate and encoding_instantiate if an enumeration type is kept.
b3b17c6c