Hi, I made a quick experiment at moving the
constructor tactic to the new proof engine and to
evarconv. This is not so easy and I'm blocking at the level of the interaction between typeclass resolution and heuristics. Probably not worth to insist at this stage knowing that that would be subsumed by unifall but I'm curious about the status of this typeclasses/heuristics interaction. What is done, and in which order, when calling a tactics (cc @Maxime Dénès , @Matthieu Sozeau)?
It does ring a bell. I don't recall exactly where we were with
Already when porting clenvs to evarconv,
constructor had shown some subtle behavior changes, IIRC.
It would be nice if the user had control over what is considered a constructor. For inductive types, its a no brainer, but for records, sometimes you might want a "smart constructor". If we could somehow label definitions (perhaps with an attribute) we could override what is considered "Build_X" for X. Also finer control, like we have for
refine would be nice
Last updated: Dec 01 2023 at 07:01 UTC