[isabelle] 1/0 = 0?



Hi,

I was recently confused about expressions such as value "(1::nat)/0"
for which I get the result 0 :: real.

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?

Kind regards
Manfred




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