Documentation

Aesop.Script.UScript

source
@[reducible, inline]
abbrev Aesop.Script.UScript :
Type
Equations
    Instances For
      source
      def Aesop.Script.UScript.render {m : Type → Type} [Monad m] [Lean.MonadError m] (tacticState : TacticState) (s : UScript) :
      m (Array Lean.Syntax.Tactic)
      Equations
        Instances For
          source
          def Aesop.Script.UScript.renderTacticSeq (uscript : UScript) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) :
          Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
          Equations
            Instances For
              source
              def Aesop.Script.UScript.validate (s : UScript) :
              Lean.MetaM Unit
              Equations
                Instances For