Documentation

Aesop.Script.UScript

source
@[reducible, inline]
abbrev Aesop.Script.UScript :
Type
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)
    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)
      Instances For
        source
        def Aesop.Script.UScript.validate (s : UScript) :
        Lean.MetaM Unit
        Instances For