HepLean Documentation

Aesop.Script.Main

source
def Aesop.Script.UScript.optimize (uscript : Aesop.Script.UScript) (proofHasMVar : Bool) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) :
Lean.MetaM (Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq × Aesop.ScriptGenerated))
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Aesop.Script.UScript.optimize.structureStatic (uscript : Aesop.Script.UScript) (proofHasMVar : Bool) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) :
    Lean.MetaM (Option (Aesop.Script.SScript × Aesop.ScriptGenerated))
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Aesop.Script.UScript.optimize.structureDynamic (uscript : Aesop.Script.UScript) (proofHasMVar : Bool) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) :
      Lean.MetaM (Option (Aesop.Script.SScript × Aesop.ScriptGenerated))
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Aesop.checkAndTraceScript {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.MonadRef m] [Lean.MonadError m] [Lean.AddMessageContext m] [Aesop.MonadStats m] [MonadLiftT Lean.MetaM m] (uscript : Aesop.Script.UScript) (sscript? : Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq × Aesop.ScriptGenerated)) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) (options : Aesop.Options') (expectCompleteProof : Bool) (tacticName : String) :
        m Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For