Documentation

Aesop.Script.Main

source
def Aesop.Script.UScript.optimize (uscript : UScript) (proofHasMVar : Bool) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) :
Lean.MetaM (Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq × ScriptGenerated))
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Aesop.Script.UScript.optimize.structureStatic (uscript : UScript) (proofHasMVar : Bool) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) :
    Lean.MetaM (Option (SScript × ScriptGenerated))
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Aesop.Script.UScript.optimize.structureDynamic (uscript : UScript) (proofHasMVar : Bool) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) :
      Lean.MetaM (Option (SScript × 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] [MonadStats m] [MonadLiftT Lean.MetaM m] (uscript : Script.UScript) (sscript? : Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq × ScriptGenerated)) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) (options : Options') (expectCompleteProof : Bool) (tacticName : String) :
        m Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For