class Lean.Grind.ToInt (α : Type u) : Type

TODO: delete this class (and this file) after the next update-stage0. The current stage0 binary's getToIntId? still resolves the constant Lean.Grind.ToInt by name while building the stage1 library; the class only needs to exist, no instances.