- cache : Lean.HashMapImp Lean.Expr Bool
Instances For
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.
Instances For
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 : Lean.HasConstCache declName) => match x with | { cache := cache } => { cache := (cache.insert e r).fst } pure r
Instances For
@[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.