Recursive Definitions in Lean (bobkonf2025)

The logic underlying the Lean programming language and theorem prover 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. (This spontaneous talk is based on the talk given at Leaning in 2025.) The material presented can be found at https://github.com/nomeata/lean-bobkonf-2025. Licensed to the public under https://creativecommons.org/licenses/by/3.0/de about this event: https://bobkonf.de/2025/breitner.html