On Fri, Apr 3, 2020 at 12:12 PM Olivier Binda <[email protected]> wrote:
> So far, I have only changed c1 into 1 (same for c2, c3, c4, c5, c6, c7, > c8, c10). Which requires > to replace every instance of "c1" in the mmu and mm0 files with "1" (some > work, but not very hard) > Note that "1" is not a valid mm0 identifier. You have to define "1" as a notation for a constant with a valid identifier, such as "c1". and added simple notations for the logical operators (this is even easier) > > but now, I'll try to do something hard : > - either replace the term for logical or with a definition (which means > refactoring lots of proofs) > - or replacing the co usage for +, with using a term (which probably means > more refactoring) > The MM0 pretty printer already knows how to print notations, so all you would have to do is to add a notation for wo. But it would have to happen between reading the incoming .mm file and producing the output, that is, inside mm0-hs, so that is on me to some extent. It needs to somehow accept configuration information to guide the process, and passing that by the command line would be very clunky. The internal metamath parser already knows how to read $j commands, so one option would be to add a new $j command declaring the notation. I am not at all sure that I'll be able to pull this off. I do not know how > long it will take me either. > (I only know that if I can pull this off, I'll be able to improve stuff a > lot) > > I'll probably go with replacing the or term with a definition (which will > make me able to write conversibility proof, a necessary requirement for me). > Doing this alone is pretty easy, especially if you are doing manual fixups on the output file. Put the definition of or in for "def wo", and prove df_or by reflexivity (after unfolding) Mario . > > Wish me luck ! > > Best regards, > Olivier > ps : I'll soon publish my patched mm0/mmu files (in case someone is > interested) ans also my mm0/mmu parsers (first). > Those can/should still be improved but it can be done later. > > > Stay home and stay safe ! :) > > -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/65485950-3987-4be2-8746-cf1e93df5267%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/65485950-3987-4be2-8746-cf1e93df5267%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuDSNY%2B0SUcwiwxgjuL6F%3DTX9GTwjXo5Sr%3Dx60D-C2rcA%40mail.gmail.com.
