partial def Aesop.optimizeFocusRenameI {m : Type → Type} [Monad m] [Lean.MonadQuotation m] : Lean.Syntax → m Lean.Syntax

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.

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

• One or more equations did not get rendered due to their size.

def Aesop.optimizeSyntax {m : Type → Type} [Monad m] [Lean.MonadQuotation m] {kind : Lean.SyntaxNodeKinds} (stx : Lean.TSyntax kind) : m (Lean.TSyntax kind)

Equations

• Aesop.optimizeSyntax stx = do let r ← Aesop.optimizeFocusRenameI stx.raw let stx : Lean.Syntax := r let r ← Aesop.optimizeInitialRenameI stx let stx : Lean.Syntax := r pure { raw := stx }