@[inline]

abbrev Lean.Expr.ReplaceImpl.cacheSize : USize

Equations

• Lean.Expr.ReplaceImpl.cacheSize = 8192

structure Lean.Expr.ReplaceImpl.State : Type

• keys : Array Lean.Expr
• results : Array Lean.Expr

@[inline]

abbrev Lean.Expr.ReplaceImpl.ReplaceM (α : Type) : Type

Equations

• Lean.Expr.ReplaceImpl.ReplaceM = StateM Lean.Expr.ReplaceImpl.State

unsafe def Lean.Expr.ReplaceImpl.cache (i : USize) (key : Lean.Expr) (result : Lean.Expr) : Lean.Expr.ReplaceImpl.ReplaceM Lean.Expr

Equations

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

unsafe def Lean.Expr.ReplaceImpl.replaceUnsafeM (f? : Lean.Expr → Option Lean.Expr) (size : USize) (e : Lean.Expr) : Lean.Expr.ReplaceImpl.ReplaceM Lean.Expr

Equations

• Lean.Expr.ReplaceImpl.replaceUnsafeM f? size e = Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size e

unsafe def Lean.Expr.ReplaceImpl.replaceUnsafeM.visit (f? : Lean.Expr → Option Lean.Expr) (size : USize) (e : Lean.Expr) : Lean.Expr.ReplaceImpl.ReplaceM Lean.Expr

Equations

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

unsafe def Lean.Expr.ReplaceImpl.initCache : Lean.Expr.ReplaceImpl.State

Equations

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

unsafe def Lean.Expr.ReplaceImpl.replaceUnsafe (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr

Equations

• Lean.Expr.ReplaceImpl.replaceUnsafe f? e = StateT.run' (Lean.Expr.ReplaceImpl.replaceUnsafeM f? Lean.Expr.ReplaceImpl.cacheSize e) Lean.Expr.ReplaceImpl.initCache

@[implementedBy Lean.Expr.ReplaceImpl.replaceUnsafe]

partial def Lean.Expr.replace (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr