Recursors and implementation

Stream: new members

[Graham Leach-Krouse]

Naive question about lean4 implementation. Are all recursive definitions and inductive proofs elaborated into code that only uses recursors? This comment suggests that's the case: https://github.com/leanprover/lean4/blob/b4ff5455baedabc644f30a0e08f679db139ebf74/src/Lean/Declaration.lean#L116, but I'm curious if there's anything more subtle going on.

[Kyle Miller]

Yes, and you can #print a definition to see what it eventually elaborated to.

The compiler that emits C code sees the "pre-definitions" though, which still have recursion. The process of turning pre-definitions into definitions, what the kernel sees, is independent of this. As far as compilation is concerned, this elaboration process is the termination checking step.

[Graham Leach-Krouse]

Excellent, thanks!