Documentation

Lean.Util.HasConstCache

structure Lean.HasConstCache (declNames : Array Lake.Name) :
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Instances For
        @[implemented_by Lean.HasConstCache.containsUnsafe]

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