structure Lean.Expr.ReplaceImpl.Cache : Type

• size : USize
• keysResults : Array NonScalar

unsafe def Lean.Expr.ReplaceImpl.Cache.new (e : Lean.Expr) : Lean.Expr.ReplaceImpl.Cache

@[inline]

unsafe def Lean.Expr.ReplaceImpl.Cache.keyIdx (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) : USize

@[inline]

unsafe def Lean.Expr.ReplaceImpl.Cache.resultIdx (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) : USize

@[inline]

unsafe def Lean.Expr.ReplaceImpl.Cache.hasResultFor (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) : Bool

@[inline]

unsafe def Lean.Expr.ReplaceImpl.Cache.getResultFor (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) : Lean.Expr

unsafe def Lean.Expr.ReplaceImpl.Cache.store (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) (result : Lean.Expr) : Lean.Expr.ReplaceImpl.Cache

@[inline, reducible]

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

@[inline]

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

@[specialize #[]]

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

@[specialize #[]]

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

@[inline]

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

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Expr.replaceNoCache f? e = match f? e with | some eNew => eNew | none => e

@[implemented_by Lean.Expr.ReplaceImpl.replaceUnsafe]

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