Documentation

Aesop.Script.Main

source
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
    source
    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) :
    Lean.MetaM Unit
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For