Commit 2023-07-27 17:38 66659071

feat: says tactic combinator (#5980) This is a primitive implementation of the says combinator discussed at today's porting meeting. If you write X says, where X is a tactic that produces a "Try this: Y" message, then you will get a message "Try this: X says Y". Once you've clicked to replace X says with X says Y, after then X says Y will only run Y. I think this is already potentially useful. Possible additions:

• a CI mode that re-verifies that X really does still say Y. (Edit: DONE)
• If X doesn't say anything, perhaps implicitly wrap it with show_term?
• Add an extra suggest flag to the TacticM state, so we can instruct tactics to print "Try this:" suggestions without adding ? directly. Very happy if anyone wants to hack on this / replace with a better implementation, etc.