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
  • One or more equations did not get rendered due to their size.
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
    • One or more equations did not get rendered due to their size.
    Instances For