I presume though that Mathlib does not define the extended naturals? If they did then 1:N / 0:N would be valued at this infinity.

What I found interesting about the Scott encoding was that natural infinity was trivial to define, and arises directly from a straightforward construction of the div function (for naturals).

The encoding is as follows (\x indicates lambda abstraction for identifier x. Recursion is assumed, of course it could be made explicit with the Y combinator):

  zero := \f \x n
  succ := \n \f \x f n

  infinite := \n succ (infinite n)
  infinity := infinite zero

  subn := \n \m m (\p n (\q subn q p) n) n

  divn := \n \m (subn m n) (\p zero) (succ (divn (subn n m) m))

  divn (succ zero) zero => infinity

EDIT: Note that infinity does not have a normal form (does not terminate), but:

  subn n infinity => zero

The extended reals can also arise directly from the definition of reals either as Cauchy sequences of rationals (as unbounded increasing sequences, etc) or Dedekind cuts (let the lower cut contain all rationals) :) for reals IIRC the main reason to exclude the extended reals is to make it a field.

However I don't think any of this matters for the point the article made. The problem is not that 1:N/0:N has "nothing sensible" to return, the problem is that if you define it in the way most mathematicians do, a lot of your proofs will be littered with (inline) lemmas showing that the result of such-and-such a division is a finite natural / finite real. This is analogous the problem brought up in the article of having proofs littered with lemmas showing that the result of such-and-such a square root was real.

In fact, there is also a type `enat` in mathlib. However, have `x/y` be a term of a type that is not the type of `x` and `y` comes with it's own sets of problems. It doesn't compose as smoothly as homogeneous division.