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.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.
    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