Native algebraic data types even in the presence of polymorphism
- Added support for new metas for the eliminate_algebraic transform, letting control which types are eliminated and which are not.
- In discriminate, added support for algebraic datatypes : duplicate propositions using algebraic datatypes to specialise algebraic datatypes instances. Then, it produces the new meta for instructing eliminate_algebraic to keep these instantiated datatypes.
- Discrimination is now performed after eliminate_algebraic
- Added support for algebraic datatypes in the polymorphism encoding.
- Fixed sessions in examples
- Simpify some sessions in examples to show that we are indeed gaining some proof power
There has been a few regressions: some old provers did not appreciate that we remove axioms about Booleans telling essentially that true != false. I fixed the corresponding proofs. Nightly works now fully.
Remaining problem to solve:
-
The CE bench of CI is not working correctly, and I don't really understand what is happening and whether this is a real problem. We need to talk about this.