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

Equations

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

@[inline]

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

Equations

• Lean.Expr.ReplaceImpl.Cache.keyIdx c key = ptrAddrUnsafe key % c.size

@[inline]

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

Equations

• Lean.Expr.ReplaceImpl.Cache.resultIdx c key = Lean.Expr.ReplaceImpl.Cache.keyIdx c key + c.size

@[inline]

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

Equations

• Lean.Expr.ReplaceImpl.Cache.hasResultFor c key = let_fun this := ⋯; ptrEq (unsafeCast key) c.keysResults[Lean.Expr.ReplaceImpl.Cache.keyIdx c key]

@[inline]

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

Equations

• Lean.Expr.ReplaceImpl.Cache.getResultFor c key = let_fun this := ⋯; unsafeCast c.keysResults[Lean.Expr.ReplaceImpl.Cache.resultIdx c key]

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, reducible]

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) => 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 e)

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