HepLean Documentation

Lean.Util.HasConstCache

source
structure Lean.HasConstCache (declNames : Array Lake.Name) :
Type
Instances For
    source
    unsafe def Lean.HasConstCache.containsUnsafe {declNames : Array Lake.Name} (e : Lean.Expr) :
    StateM (Lean.HasConstCache declNames) Bool
    Instances For
      source
      unsafe def Lean.HasConstCache.containsUnsafe.cache {declNames : Array Lake.Name} (e : Lean.Expr) (r : Bool) :
      StateM (Lean.HasConstCache declNames) Bool
      Instances For
        source
        @[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.