Hacker News Reader

The standard arithmetic classes of Isabelle/HOL show that you can extend division with the equation `x / 0 = 0` and things (seemingly) work out.

https://lawrencecpaulson.github.io/2021/12/01/Undefined.html

https://www.hillelwayne.com/post/divide-by-zero/

https://xenaproject.wordpress.com/2020/07/05/division-by-zer...

You'll need to do some thinking/proof to find out if it works for you.

View on HN

Huh. That's surprising but quite persuasive, thank you for the references. I like the general view that a non-axiomatic divide can't introduce unsoundness so define it however is useful.

It has somewhat kicked the can down the road to defining the multiplicative inverse, but that's still a good step forward. Thank you

Reply on news.ycombinator.com