Documentation

Lean.Util.ReplaceLevel

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

@[inline, reducible]

abbrev Lean.Expr.ReplaceLevelImpl.cacheSize :

Equations

Lean.Expr.ReplaceLevelImpl.cacheSize = 8192 - 1

Instances For

structure Lean.Expr.ReplaceLevelImpl.State :

keys : Array Lean.Expr
results : Array Lean.Expr

Instances For

@[inline, reducible]

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

Equations

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

Instances For

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

Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr

Equations

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

Instances For

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

Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr

Equations

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

Instances For

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

Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr

Equations

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

Instances For

unsafe def Lean.Expr.ReplaceLevelImpl.initCache :

Lean.Expr.ReplaceLevelImpl.State

Equations

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

Instances For

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

Equations

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

Instances For

@[implemented_by Lean.Expr.ReplaceLevelImpl.replaceUnsafe]

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

Lean.Expr → Lean.Expr