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