Re: [isabelle] Infinity - infinity = infinity

Johannes wrote:

> Are you sure your definition works?

Not anymore. ;) Nitpick finds counterexamples for pretty much any property I hoped to have. Clearly, I could have spared myself some embarrassment by firing up this tool earlier.

What I'll take home from this is that subtraction on "enat" is necessarily a messy business.


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