Documentation

Aesop.Script.StructureStatic

source
🔶 coverage
structure Aesop.Script.StaticStructureM.State :
Type
  • perfect : Bool
Instances For
    source
    🔶 coverage
    structure Aesop.Script.StaticStructureM.Context :
    Type
    • steps : Std.HashMap Lean.MVarId (Nat × Step)
    Instances For
      source
      🔸 coverage
      @[reducible, inline]
      abbrev Aesop.Script.StaticStructureM (α : Type) :
      Type
      Equations
      Instances For
        source
        🔸 coverage
        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
          🔸 coverage
          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
            🔸 coverage
            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