fix: matcher splitter is code

It have to keep it as a private definition for now.
We currently only support duplicate theorems in different modules.
Splitters are generated on demand, and are also used to write code.