@[inline]

def Lean.Expr.ReplaceImpl.cacheSize : USize

Equations

• Lean.Expr.ReplaceImpl.cacheSize = 8192 - 1

structure Lean.Expr.ReplaceImpl.Cache : Type

• keysResults : Array NonScalar

unsafe def Lean.Expr.ReplaceImpl.Cache.new : Lean.Expr.ReplaceImpl.Cache

Equations

• Lean.Expr.ReplaceImpl.Cache.new = { keysResults := mkArray (USize.toNat (2 * Lean.Expr.ReplaceImpl.cacheSize)) (unsafeCast ()) }

@[inline]

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

Equations

• Lean.Expr.ReplaceImpl.Cache.keyIdx key = ptrAddrUnsafe key % Lean.Expr.ReplaceImpl.cacheSize

@[inline]

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

Equations

• Lean.Expr.ReplaceImpl.Cache.resultIdx key = Lean.Expr.ReplaceImpl.Cache.keyIdx key + Lean.Expr.ReplaceImpl.cacheSize

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Expr.ReplaceImpl.cache key result = do modify fun x => Lean.Expr.ReplaceImpl.Cache.store x key result pure result

@[specialize #[]]

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

Equations

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

@[specialize #[]]

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

Equations

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

@[inline]

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? e) Lean.Expr.ReplaceImpl.Cache.new

@[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

Equations

• Lean.Expr.replace f? e = Lean.Expr.replaceNoCache f? e