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
    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
        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
            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
                Instances For