Documentation

Aesop.Script.OptimizeSyntax

source
partial def Aesop.optimizeFocusRenameI {m : Type → Type} [Monad m] [Lean.MonadQuotation m] :
Lean.Syntax → m Lean.Syntax
source
def Aesop.optimizeInitialRenameI {m : Type → Type} [Monad m] [Lean.MonadQuotation m] :
Lean.Syntax → m Lean.Syntax
Equations
    Instances For
      source
      def Aesop.optimizeInitialRenameI.tacsToTacticSeq {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (tacs : Array (Lean.TSyntax `tactic)) :
      m (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
      Equations
        Instances For
          source
          def Aesop.optimizeSyntax {m : Type → Type} [Monad m] [Lean.MonadQuotation m] {kind : Lean.SyntaxNodeKinds} (stx : Lean.TSyntax kind) :
          m (Lean.TSyntax kind)
          Equations
            Instances For