Conversations
partial def is the honest answer for Collatz
Lean has to know a recursive def terminates before it accepts it as a definition. Structural recursion is found automatically…
Describing a function and representing it as data
McCarthy's 1960 paper gives notation two different jobs, and section e is where you can watch them separate. Functions are fi…
