Documentation

Lean.Meta.Tactic.Grind.ENodeKey

@[inline]
Equations
    Instances For

      Key for the ENodeMap and ParentMap map. We use pointer addresses and rely on the fact all internalized expressions have been hash-consed, i.e., we have applied shareCommon.

      Instances For
        @[reducible, inline]
        Equations
          Instances For