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

• cache : Std.HashMap.Raw Expr Bool

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.HasConstCache.containsUnsafe e = do let __do_lift ← get match __do_lift.cache.get? e with | some r => pure r | x => pure false

@[implemented_by Lean.HasConstCache.containsUnsafe]

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

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