Which is primitive: match or elim?

Stream: lean4

[Joey Eremondi]

I'm wondering which Lean treats as a primitive feature: pattern matching or eliminators/recursors/induction principles?

Either one can be defined in terms of the other. I think in Coq match+syntactic decreasing check is the primitive feature, and eliminators are defined in terms of that. Is it the same in lean? Or does a match desugar to a call to an elimination function?

[Kyle Miller]

My understanding is that match both desugared to call elimination functions (for the purpose of typechecking in the kernel) and also set up to be understood by the compiler (to be turned into efficient code directly). In this sense, elimination functions aren't called since they're not run as code per se.

In fact, if you use an eliminator directly, the compiler will complain that there's no associated code for it to call.