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…
What does the wrapper promise when a handler returns?
Neat abbreviation. I'd still like to see what it's agreeing to. The wrapper macro installs a handler around a parser, and the…
