inductive Aesop.SyntaxMap.Key : Type

• node: Lean.SyntaxNodeKind → Aesop.SyntaxMap.Key
• atom: String → Aesop.SyntaxMap.Key
• ident: Lean.Name → Aesop.SyntaxMap.Key

instance Aesop.SyntaxMap.instInhabitedKey : Inhabited Aesop.SyntaxMap.Key

Equations

• Aesop.SyntaxMap.instInhabitedKey = { default := Aesop.SyntaxMap.Key.node default }

instance Aesop.SyntaxMap.instBEqKey : BEq Aesop.SyntaxMap.Key

Equations

• Aesop.SyntaxMap.instBEqKey = { beq := Aesop.SyntaxMap.beqKey✝ }

instance Aesop.SyntaxMap.instHashableKey : Hashable Aesop.SyntaxMap.Key

Equations

• Aesop.SyntaxMap.instHashableKey = { hash := Aesop.SyntaxMap.hashKey✝ }

instance Aesop.SyntaxMap.Key.instToString : ToString Aesop.SyntaxMap.Key

Equations

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

def Aesop.SyntaxMap.Key.ofSyntax : Lean.Syntax → Option Aesop.SyntaxMap.Key

Equations

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

structure Aesop.SyntaxMap (α : Type u_1) : Type u_1

• toPHashMap : Lean.PHashMap Aesop.SyntaxMap.Key α

instance Aesop.instInhabitedSyntaxMap : {a : Type u_1} → Inhabited (Aesop.SyntaxMap a)

Equations

• Aesop.instInhabitedSyntaxMap = { default := { toPHashMap := default } }

structure Aesop.SyntaxRewrite : Type

• keys : Array Aesop.SyntaxMap.Key
• run : Lean.Syntax → Lean.CoreM (Option Lean.Syntax)

instance Aesop.instInhabitedSyntaxRewrite : Inhabited Aesop.SyntaxRewrite

Equations

• Aesop.instInhabitedSyntaxRewrite = { default := { keys := default, run := default } }

def Aesop.SyntaxMap.empty {α : Type u_1} : Aesop.SyntaxMap α

Equations

• Aesop.SyntaxMap.empty = { toPHashMap := Lean.PersistentHashMap.empty }

instance Aesop.SyntaxMap.instEmptyCollection {α : Type u_1} : EmptyCollection (Aesop.SyntaxMap α)

Equations

• Aesop.SyntaxMap.instEmptyCollection = { emptyCollection := Aesop.SyntaxMap.empty }

def Aesop.SyntaxMap.find? {α : Type u_1} (key : Aesop.SyntaxMap.Key) (m : Aesop.SyntaxMap α) : Option α

Equations

• Aesop.SyntaxMap.find? key m = Lean.PersistentHashMap.find? m.toPHashMap key

def Aesop.SyntaxMap.findStx? {α : Type} (stx : Lean.Syntax) (m : Aesop.SyntaxMap α) : Option α

Equations

• Aesop.SyntaxMap.findStx? stx m = do let key ← Aesop.SyntaxMap.Key.ofSyntax stx Aesop.SyntaxMap.find? key m

def Aesop.SyntaxMap.insert {α : Type u_1} (key : Aesop.SyntaxMap.Key) (val : α) (m : Aesop.SyntaxMap α) : Aesop.SyntaxMap α

Equations

• Aesop.SyntaxMap.insert key val m = { toPHashMap := Lean.PersistentHashMap.insert m.toPHashMap key val }

@[macro_inline]

def Aesop.SyntaxMap.insertWith {α : Type u_1} (key : Aesop.SyntaxMap.Key) (a : α) (f : α → α) (m : Aesop.SyntaxMap α) : Aesop.SyntaxMap α

Equations

• Aesop.SyntaxMap.insertWith key a f m = match Aesop.SyntaxMap.find? key m with | some a' => Aesop.SyntaxMap.insert key (f a') m | none => Aesop.SyntaxMap.insert key a m

@[reducible, inline]

abbrev Aesop.SyntaxRewriteMap : Type

Equations

• Aesop.SyntaxRewriteMap = Aesop.SyntaxMap (List Aesop.SyntaxRewrite)

def Aesop.SyntaxRewriteMap.insert (rw : Aesop.SyntaxRewrite) (m : Aesop.SyntaxRewriteMap) : Aesop.SyntaxRewriteMap

Equations

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

def Aesop.optimizeSyntaxWith (rws : Aesop.SyntaxRewriteMap) (stx : Lean.Syntax) : Lean.CoreM Lean.Syntax

Equations

• Aesop.optimizeSyntaxWith rws stx = Aesop.optimizeSyntaxWith.go rws stx

partial def Aesop.optimizeSyntaxWith.go (rws : Aesop.SyntaxRewriteMap) (stx : Lean.Syntax) : Lean.CoreM Lean.Syntax

def Aesop.optimizeSyntaxWith.optimizeHead (rws : Aesop.SyntaxRewriteMap) (stx : Lean.Syntax) : Lean.CoreM Lean.Syntax

Equations

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

def Aesop.SyntaxRewrite.focusRenameI : Aesop.SyntaxRewrite

Equations

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

def Aesop.optimizeSyntax {kind : Lean.SyntaxNodeKinds} (stx : Lean.TSyntax kind) : Lean.CoreM (Lean.TSyntax kind)

Equations

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