a tactic that does not need to backtrack

Stream: Is there code for X?

[Paige Thomas]

Is there a nonclosing tactic that will apply all of the tactics that would never need to backtrack? For example, splitting and, or and iff in the hypotheses, existential elimination of existential formulas in the hypothesis, calling intro on implication and forall in the goal, substituting equalities in the hypotheses, splitting if, then, else, etc.? And maybe a way to tag tactics for its use?

[Yaël Dillies]

That sounds like aesop configured to be safe

[Paige Thomas]

oh?

[Paige Thomas]

I'll take a look. Thank you!

[Yaël Dillies]

Something like aesop (config := { warnOnNonterminal := false, enableSimp := false })

[Yaël Dillies]

You will want to have a look at docs#Aesop.Options

[Paige Thomas]

Is there an intro guide to aesop in general?

[Yaël Dillies]

Eh, not really. Best it to ask Jannis Limperg

[Yaël Dillies]

There is a paper about it and also talks, eg https://limperg.de/talk/bicmr-202404/slides.pdf

[Paige Thomas]

Ok. Thank you.

[Kevin Buzzard]

I have found the project README (linked to in the module docstring) very informative as an intro guide