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 constructor
, though.
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 simple
, notypeclasses
etc.
Last updated: Oct 13 2024 at 01:02 UTC