Documentation

Aesop.Script.StructureStatic

source
structure Aesop.Script.StaticStructureM.State :
Type
Instances For
    source
    structure Aesop.Script.StaticStructureM.Context :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev Aesop.Script.StaticStructureM (α : Type) :
      Type
      Equations
        Instances For
          source
          def Aesop.Script.StaticStructureM.run {α : Type} (script : UScript) (x : StaticStructureM α) :
          Lean.CoreM (α × Bool)
          Equations
            Instances For
              source
              def Aesop.Script.structureStaticCore (tacticState : TacticState) (script : UScript) :
              Lean.CoreM (UScript × Bool)
              Equations
                Instances For
                  source
                  partial def Aesop.Script.structureStaticCore.go (tacticState : TacticState) :
                  StaticStructureM (List Step × TacticState)
                  source
                  def Aesop.Script.structureStaticCore.nextStep (tacticState : TacticState) (mainGoal : GoalWithMVars) :
                  StaticStructureM Step
                  Equations
                    Instances For
                      source
                      def Aesop.Script.UScript.toSScriptStatic (tacticState : TacticState) (uscript : UScript) :
                      Lean.CoreM (SScript × Bool)
                      Equations
                        Instances For