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