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.
Instances For
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 have stx : Lean.Syntax := r let r ← Aesop.optimizeInitialRenameI stx have stx : Lean.Syntax := r pure { raw := stx }