Guillaume Melquiond

> With only the features proposed in the CEP, a user can manually check a candidate for a propositional realization. This amounts to translating each equation `lhs = rhs` into...

> rewrite rules will still be able to add potential non-termination. Sure, and that is perfectly fine with me, as long as we can promise soundness to our users. They...

> Indeed, as our criterion requires freshness of the symbol, one would not have any chance of proving any equality about it. I never suggested that the equalities had to...

> In cases where realisation is impossible because we want to extend the theory, then we might have to add as many axioms as there are symbols and rewrite rules...

> I vaguely remember reading ANSSI recommendations about `Axiom` that were sensibly more nuanced than "never use the feature ever" So, let me remind those recommendations: 1. Developers are only...

> If I understand correctly, then when printing the assumptions for plus or any term depending on it / and its rewrite rules, we would list `ax_plus` besides `plus_O_n` etc....

> We could try to remove match on primitive records and see how much incompatibilities it induces? I think it is a bad idea. Not only would it break existing...

By the way, it seems there is a design decision you did not consider (or I missed it): - forbid partially applied primitive projections. The syntax `f params c` would...

> That’s only true if users are writing those matches by hand (personally never seen that) As a point of data, there are 93 such match constructs in CoqInterval and...

For 1:2.3 (controlling delta depending on the number of arguments), I wonder whether it would work to declare the projection as a fixpoint in its last argument. The delta rule...