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.optimizeSyntax {m : Type → Type} [Monad m] [Lean.MonadQuotation m] {kind : Lean.SyntaxNodeKinds} (stx : Lean.TSyntax kind) :
      m (Lean.TSyntax kind)
      Equations
        Instances For