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

@[reducible, inline]

abbrev Lean.Expr.ReplaceLevelImpl.cacheSize : USize

Equations

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

structure Lean.Expr.ReplaceLevelImpl.State : Type

• keys : Array Lean.Expr
• results : Array Lean.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 : Lean.Expr) (result : Lean.Expr) : Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr

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

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

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

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

@[implemented_by Lean.Expr.ReplaceLevelImpl.replaceUnsafe]

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