Documentation

Aesop.Script.ScriptM

source
@[reducible, inline]
abbrev Aesop.ScriptT (m : Type → Type) (α : Type) :
Type
Equations
    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)
      Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Aesop.ScriptM (α : Type) :
          Type
          Equations
            Instances For
              source
              def Aesop.recordScriptStep {m : Type → Type u_1} [MonadStateOf (Array Script.LazyStep) m] (step : Script.LazyStep) :
              m Unit
              Equations
                Instances For
                  source
                  def Aesop.recordScriptSteps {m : Type → Type u_1} [MonadStateOf (Array Script.LazyStep) m] (steps : Array Script.LazyStep) :
                  m Unit
                  Equations
                    Instances For
                      source
                      def Aesop.withScriptStep {α : Type} (preGoal : Lean.MVarId) (postGoals : α → Array Lean.MVarId) (success : α → Bool) (tacticBuilder : α → Script.TacticBuilder) (x : Lean.MetaM α) :
                      ScriptM α
                      Equations
                        Instances For
                          source
                          def Aesop.withOptScriptStep {α : Type} (preGoal : Lean.MVarId) (postGoals : α → Array Lean.MVarId) (tacticBuilder : α → Script.TacticBuilder) (x : Lean.MetaM (Option α)) :
                          ScriptM (Option α)
                          Equations
                            Instances For