Documentation

Lean.Util.HasConstCache

source
structure Lean.HasConstCache (declName : Lake.Name) :
Type
source
unsafe def Lean.HasConstCache.containsUnsafe {declName : Lake.Name} (e : Lean.Expr) :
StateM (Lean.HasConstCache declName) Bool
Equations
  • One or more equations did not get rendered due to their size.
source
unsafe def Lean.HasConstCache.containsUnsafe.cache {declName : Lake.Name} (e : Lean.Expr) (r : Bool) :
StateM (Lean.HasConstCache declName) Bool
Equations
  • One or more equations did not get rendered due to their size.
source
@[implemented_by Lean.HasConstCache.containsUnsafe]
opaque Lean.HasConstCache.contains {declName : Lake.Name} (e : Lean.Expr) :
StateM (Lean.HasConstCache declName) Bool

Return true iff e contains the constant declName. Remark: the results for visited expressions are stored in the state cache.