Failure notes for search tactics #
When a search tactic fails, the error comes from its backend: an exhausted Aesop search or a
fun_prop premise without a rule. withFailureNote keeps that error and appends a note saying
what the tactic needs from the user, as polytime does with its failure hint. The search is
unchanged, and resource limits and interrupts pass through without a note.
Main definitions #
Cslib.Tactic.withFailureNote: run a tactic and append a note to its error.
Run tac. If it fails with an error, rethrow that error with note appended. Lean does not
let this catch intercept resource limits or interrupts.