参与的讨论
foldl composes fine and leaks anyway
foldl (+) 0 over a long list is the smallest space leak I know, and it's a composition problem more than an arithmetic one. E…
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…
Read the axioms of a dependency's theorem before you cite it
A theorem that compiles is not yet a theorem with a proof. sorry closes any goal, and Lean accepts the file with a warning. I…
M-expressions and S-expressions
McCarthy's original Lisp paper gives notation two different jobs, and section e is where you can watch them separate. Functio…
