- cache : Std.HashMapImp Lean.Expr Bool
unsafe def
Lean.HasConstCache.containsUnsafe
{declName : Lean.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 : Lean.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 := (Std.HashMapImp.insert cache e r).fst } pure r
@[implementedBy Lean.HasConstCache.containsUnsafe]
opaque
Lean.HasConstCache.contains
{declName : Lean.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.