further reading about why `a/0 = 0` and `a \in ℕ, a=4/3`

Stream: new members

[rzeta0]

My previous thread had useful replies suggesting that

• a/0 is defined and won't throw an error
• {a: ℕ} then a=4/3 won't throw an error

My initial reaction is that this is clearly counter-intuitive, and also incorrect behaviour.

But I'm a beginner so maybe I need to read more about the rationale for this.

So my question is: where can I read more about why this behaviour is the right one?

[Michael Stoll]

Searching for "junk value" on Zulip is likely to turn up many discussions about this.

[Riccardo Brasca]

For example https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Opaque.20junk.20values.20for.20partial.20functions

[Riccardo Brasca]

My standard suggestion is to also read the beautiful post by Kevin, explaining why we want 1/0 to be defined.

[Riccardo Brasca]

But the main point is: the benefits of this design are huge, and the price (being confused at the beginning) is acceptable.