grind and sizeOf_spec

Stream: lean4

[Chris Henson]

Could someone help me understand how grind interacts (or doesn't) with sizeOf_spec theorems? In doing termination_by proofs it appears you need to manually specify these to grind, wheras they already are marked as simp automatically. But I also see a #grind_lint skip suffix sizeOf_spec in the lean4 repo, so maybe there is some interaction?

[Théophile]

They should now be marked for grind, see this recent PR https://github.com/leanprover/lean4/pull/11265