Re: [isabelle] Cl-isabelle-users Digest, Vol 138, Issue 4



What will be the type of "-" in that case?
Do you really want to go there?

On 12/02/2016 05:26 PM, W. Douglas Maurer wrote:
> Some day I hope it will be possible to implement a system that does what real computers do in this case: infinity minus infinity gives NaN, which stands for Not a Number. Then any combination of NaN with anything else also gives NaN. (See any formal description of IEEE standard floating point arithmetic.) --WDMaurer
> 
> Sent from my iPhone
> 





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