structure Lean.HasConstCache (declNames : Array Lake.Name) : Type

• cache : Std.HashMap.Raw Lean.Expr Bool

unsafe def Lean.HasConstCache.containsUnsafe {declNames : Array Lake.Name} (e : Lean.Expr) : StateM (Lean.HasConstCache declNames) Bool

unsafe def Lean.HasConstCache.containsUnsafe.cache {declNames : Array Lake.Name} (e : Lean.Expr) (r : Bool) : StateM (Lean.HasConstCache declNames) Bool

@[implemented_by Lean.HasConstCache.containsUnsafe]

opaque Lean.HasConstCache.contains {declNames : Array Lake.Name} (e : Lean.Expr) : StateM (Lean.HasConstCache declNames) Bool

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