The logic underlying Lean does not know recursive functions, yet Lean users can define functions recursively. In this session we'll get to look at how Lean translates the user's specification into something that the logic understands, whether by structural recursion, well-founded recursion or the brand-new partial fixpoint strategy. We'll also see how this affects compiled code (namely not at all), and the difference between partial and unsafe.
This session will likely contain high amounts of improvised live-coding and benefit greatly from your questions, suggestions and discussions.