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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Aesop.Script.structureStaticCore (tacticState : TacticState) (script : UScript) :
          Lean.CoreM (UScript × Bool)
          Equations
          • One or more equations did not get rendered due to their size.
          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
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Aesop.Script.UScript.toSScriptStatic (tacticState : TacticState) (uscript : UScript) :
              Lean.CoreM (SScript × Bool)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For