Back

More languages should adopt Lean's annotation of partial function definitions, even if they're not using it as a way to isolate partiality from a logic.

Function definitions that are not obviously terminating (and Lean has a pretty expansive definition of "obviously" here compared to many systems) are inherently a bit more suspect than other definitions.