def
Aesop.Script.UScript.optimize
(uscript : Aesop.Script.UScript)
(preState : Lean.Meta.SavedState)
(goal : Lean.MVarId)
:
Lean.MetaM (Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq × Bool))
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Aesop.checkAndTraceScript
(uscript : Aesop.Script.UScript)
(sscript? : Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq))
(preState : Lean.Meta.SavedState)
(goal : Lean.MVarId)
(options : Aesop.Options')
(expectCompleteProof : Bool)
(tacticName : String)
:
Equations
- One or more equations did not get rendered due to their size.