Documentation

Aesop.Script.ScriptM

source
@[reducible, inline]
abbrev Aesop.ScriptT (m : Type → Type) (α : Type) :
Type
Instances For
    source
    def Aesop.ScriptT.run {m : Type → Type} {α : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (x : ScriptT m α) :
    m (α × Array Script.LazyStep)
    Instances For
      source
      @[reducible, inline]
      abbrev Aesop.ScriptM (α : Type) :
      Type
      Instances For
        source
        def Aesop.recordScriptStep {m : Type → Type u_1} [MonadStateOf (Array Script.LazyStep) m] (step : Script.LazyStep) :
        m Unit
        Instances For
          source
          def Aesop.recordScriptSteps {m : Type → Type u_1} [MonadStateOf (Array Script.LazyStep) m] (steps : Array Script.LazyStep) :
          m Unit
          Instances For
            source
            def Aesop.withScriptStep {α : Type} (preGoal : Lean.MVarId) (postGoals : α → Array Lean.MVarId) (success : α → Bool) (tacticBuilder : α → Script.TacticBuilder) (x : Lean.MetaM α) :
            ScriptM α
            Instances For
              source
              def Aesop.withOptScriptStep {α : Type} (preGoal : Lean.MVarId) (postGoals : α → Array Lean.MVarId) (tacticBuilder : α → Script.TacticBuilder) (x : Lean.MetaM (Option α)) :
              ScriptM (Option α)
              Instances For