Hi, On Sat, Nov 09, 2019 at 11:58:08AM -0500, David A. Wheeler wrote: > > Le samedi 9 novembre 2019 12:27:12 UTC+1, Filip Cernatescu a écrit : > > > I have a question for set.mm contributors: > > > Automatic prover for a+b,a-b,a×b,a/b, a<b,a>b... it will be necessary? > mmj2 includes *some* of that. I don't know about "necessary", but it's > certainly *useful*. For completeness sake (in case anyone needs a integer-oriented automation on short notice), so does https://github.com/Drahflow/Igor
+ , - , * , ^ on NN0 should be complete <, <_, >, >_ on RR (including transitivity), should also be complete IIRC ... and of course everything in deduction-form. Regards, Drahflow -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/20191109190030.GA13548%40eta-carinae.
signature.asc
Description: PGP signature
