[FOM] 618: Adventures in Formalization 4

[Dominic Mulligan]

Dear Harvey,

Many in the theorem proving community would be likewise disgusted with a
definition of division that admitted equations like 1/0=0, or likewise,
which is why to my knowledge definitions of this form are not at all
typical in any of the major systems that I am familiar with. In dependently
typed systems like Coq, Agda or Matita the usual approach is to define
division so that it takes as argument an extra proof that the second
argument is non-zero, or equivalently define a type of non-zero integers or
reals and use that instead, and in HOL based systems like Isabelle, HOL4
and HOL Light division is left undefined in that case.

Based on your postings, I think the likes of Isabelle and Coq and the
mathematics formalised therein will be more familiar than you realise.

Thanks,
Dominic
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150917/fb1da7e1/attachment.html>