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.

Jasmin





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