structure Lean.HasConstCache (declName : Lake.Name) : Type

• cache : Lean.HashMapImp Lean.Expr Bool

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.

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

Equations

• Lean.HasConstCache.containsUnsafe.cache e r = do modify fun x => match x with | { cache := cache } => { cache := (Lean.HashMapImp.insert cache e r).fst } pure r

@[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.