Documentation

Lean.Util.HasConstCache

structure Lean.HasConstCache (declNames : Array Name) :
Instances For
    unsafe def Lean.HasConstCache.containsUnsafe {declNames : Array Name} (e : Expr) :
    Equations
      Instances For
        unsafe def Lean.HasConstCache.containsUnsafe.cache {declNames : Array Name} (e : Expr) (r : Bool) :
        Equations
          Instances For
            @[implemented_by Lean.HasConstCache.containsUnsafe]
            opaque Lean.HasConstCache.contains {declNames : Array Name} (e : Expr) :

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