lazy match splitters and lean4checker

Stream: lean4

[Joachim Breitner]

I came across this comment in the lean4 code base

/- We generate the equations and splitter on demand, and do not save them on .olean files. -/
builtin_initialize matchEqnsExt : EnvExtension MatchEqnsExtState ←
  registerEnvExtension (pure {})

If these definitions are not saved in .oleans, how does lean4checker (which, as far as I understand, just sends the definitions in the .oleans to the kernel) handle this? Are they somehow generated by lean4checker as well, or are they never even mentioned (but inlines maybe?) in the proof terms in the .olean?