News for hackers. Stuff that matters.

A comment on Division by zero in type theory: a FAQ. Parent comment

Re:Division by zero in type theory: a FAQ by thaumasiotes on Monday July 06, 2020 @04:37PM (#23752479)
Well, if you're doing a proof and (for example) you want to cancel x in the numerator of a fraction with x in the denominator, you then apply the constraint x ≠ 0 to every subsequent step of the proof.

(You may then do a separate proof in the case that x = 0, if you want to prove something for all x including 0.)

[ Parent | on HN ]
Re:Division by zero in type theory: a FAQ by zozbot234 on Monday July 06, 2020 @04:54PM (#23752649)
That's actually needed for a real proof. One should keep in mind that y = ax is not injective if a=0, so that "cancel a variable" step you're thinking of is most likely incorrect without that side-condition.
[ Parent | on HN ]
Re:Division by zero in type theory: a FAQ by thaumasiotes on Monday July 06, 2020 @05:24PM (#23752937)
...yes?
[ Parent | on HN ]