Gaëtan Gilbert (Mar 10 2021 at 16:08): Gaëtan Gilbert (Mar 10 2021 at 16:08):What do we do about https://github.com/coq/coq/issues/13834 ?
Gaëtan Gilbert (Mar 10 2021 at 16:08):cc @Pierre-Marie Pédrot
Enrico Tassi (Mar 10 2021 at 19:11):Can't we move toward having the rewrite principles declared in advance? The lazy creation/declaration of these lemmas brings very little.
I mean Error: you can't rewrite with foo unless you first run Whatever Scheme foo or decorate foo with #[rewrite].
Enrico Tassi (Mar 10 2021 at 19:12):I totally agree side effects are evil, but there are some which are kind of justified, and some others that look like they were added "for sport" like this one.
Pierre-Marie Pédrot (Mar 11 2021 at 10:03):It's even worse than that: since the rewrite side-effects are globally visible inside a Defined proof, this is a source of non-determinism.
Gaëtan Gilbert (Mar 11 2021 at 11:42):how so?
Matthieu Sozeau (Mar 12 2021 at 10:01):It's a terrible side-effect I think. And IIRC in a universe polymorphic proof it does generalize over unnecessary universes.
Enrico Tassi (Mar 12 2021 at 13:17):So, if we agree that we should generated these term ahead of time, maybe we should plan something. Still I have a memory of some cases in which there are many possible terms, and we don't know which ones (I think @Matthieu Sozeau told me this once). In any case we can design commands to generate the ones the user needs and have good error messages about what the user should run.
Last updated: May 31 2023 at 16:01 UTC