partial def Lean.Level.replace (f? : Level → Option Level) (u : Level) : Level

@[reducible, inline]

abbrev Lean.Expr.ReplaceLevelImpl.cacheSize : USize

Equations

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

structure Lean.Expr.ReplaceLevelImpl.State : Type

• keys : Array Expr
• results : Array Expr

@[reducible, inline]

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

Equations

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

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

Equations

• Lean.Expr.ReplaceLevelImpl.cache i key result = do modify fun (s : Lean.Expr.ReplaceLevelImpl.State) => { keys := s.keys.uset i key ⋯, results := s.results.uset i result ⋯ } pure result

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

Equations

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

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

Equations

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

unsafe def Lean.Expr.ReplaceLevelImpl.initCache : State

Equations

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

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

Equations

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

@[implemented_by Lean.Expr.ReplaceLevelImpl.replaceUnsafe]

partial def Lean.Expr.replaceLevel (f? : Level → Option Level) : Expr → Expr