Documentation

Lean.Util.ReplaceExpr

source
@[inline]
abbrev Lean.Expr.ReplaceImpl.cacheSize:
USize
Equations
source
structure Lean.Expr.ReplaceImpl.State:
Type
source
@[inline]
abbrev Lean.Expr.ReplaceImpl.ReplaceM (α : Type) :
Type
Equations
source
unsafe def Lean.Expr.ReplaceImpl.cache (i : USize) (key : Lean.Expr) (result : Lean.Expr) :
Lean.Expr.ReplaceImpl.ReplaceM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
unsafe def Lean.Expr.ReplaceImpl.replaceUnsafeM (f? : Lean.Expr → Option Lean.Expr) (size : USize) (e : Lean.Expr) :
Lean.Expr.ReplaceImpl.ReplaceM Lean.Expr
Equations
source
unsafe def Lean.Expr.ReplaceImpl.replaceUnsafeM.visit (f? : Lean.Expr → Option Lean.Expr) (size : USize) (e : Lean.Expr) :
Lean.Expr.ReplaceImpl.ReplaceM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
unsafe def Lean.Expr.ReplaceImpl.initCache:
Lean.Expr.ReplaceImpl.State
Equations
  • One or more equations did not get rendered due to their size.
source
unsafe def Lean.Expr.ReplaceImpl.replaceUnsafe (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) :
Lean.Expr
Equations
source
@[implementedBy Lean.Expr.ReplaceImpl.replaceUnsafe]
partial def Lean.Expr.replace (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) :
Lean.Expr