Re:You can't divide by zero – Garrit's Notes
by thaumasiotes on Saturday December 02, 2023 @11:01PM
(#38504706)
> There are good reasons for this convention in the context of Lean
There are good reasons for the convention of assigning nonsense values to computations that are formally invalid. The convention is so important that it is introduced in the Natural Number Game, where the remarks include a brief discussion of why the predecessor of 0 is defined to be 37.
I don't think there's any particular reason why you'd assign 0 as the nonsense value?
There are good reasons for the convention of assigning nonsense values to computations that are formally invalid. The convention is so important that it is introduced in the Natural Number Game, where the remarks include a brief discussion of why the predecessor of 0 is defined to be 37.
I don't think there's any particular reason why you'd assign 0 as the nonsense value?