Re: [isabelle] 1/0 = 0?



A bit of history: the first logic supported within Isabelle was Martin-Löf's constructive type theory, and it is still there (CTT). And while developing arithmetic within that formalisation, I came up with a definition (necessarily primitive recursive and executable) of division. It delivered n/0 = 0. Since then a number of people have noticed that defining x/0 = 0 is convenient. This identity holds in quite a few different proof assistants now. 

These things are conventions, exactly the same as announcing that x^-n = 1/x^n and that x^0 = 0.

Larry Paulson



> On 27 Feb 2018, at 11:02, Manfred Kerber <mnfrd.krbr at gmail.com> wrote:
> 
> I understand that the logic used in Isabelle/HOL is total. However, I
> thought that usually partiality is approximated by leaving the value
> of expressions such as 1/0 as unspecified. What is the reason that
> this seems not to be the case for 1/0?




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.