grind: internalization

Stream: lean4

[Marcus Rossel]

What does it mean for an expression to be "internalized" in grind, and which expressions are internalized?
Does "internalized" mean that the expression is represented "explicitly" in the e-graph (ie. there's an e-node n where n.self is the given expression)? If so, does that mean one would encounter it, e.g., by means of traverseEqc?

As a concrete example, consider:

set_option trace.grind.internalize true in
example (f g : Nat → Nat) (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : f a = f c := by
  grind
/-
[grind.internalize] [0] a
[grind.internalize] [0] b
[grind.internalize] [0] c
[grind.internalize] [0] f a = f c
[grind.internalize] [0] Nat
[grind.internalize] [0] f a
[grind.internalize] [0] f
[grind.internalize] [0] f c
-/

Here f a and f c are internalized (presumably because they appear explicitly in the goal f a = f c, and all subterms of internalized expressions must also be internalized?). However, the intermediate term f b is not internalized. Thus, presumably f a and f c appear explicitly in the same e-class, whereas f b is only implicitly equivalent to the previous terms by virtue of a, b and c being in the same e-class. Is that right?