Le samedi 4 avril 2020 01:23:41 UTC+2, Mario Carneiro a écrit : > > > > On Fri, Apr 3, 2020 at 12:12 PM Olivier Binda <[email protected] > <javascript:>> 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". >
Yes, you are right. I messed up (it was so in my first try but not in the second try where I changed the way things were done and I forgot about that). I will fix that as soon as possible (I want to do conforming stuff). I guess that the restriction on id is this way so that we can do nice stuff with notations (mostly with numbers). For example, at some point, I plan to allow users to write 1283 and to have that (maybe in a preprocessing step) turned into (; ; ; 1 2 8 3 ) because normal users will want to use numbers the way they are used to I messed up (not the first time, not the last time) but as always, there are benefits with failures : I have a patcher routine that allows renaming ids and propagating changes...this will be useful in the future > and added simple notations for the logical operators (this is even easier) >> >> Thanks for your guidance. > 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. > You hint that it could be done with mm0-hs. Ok. Still, I don't want to rely on that. I need to be able to do that myself, because Mephistolus needs it. So, I will only rely on mm0-hs to translate mm stuff into basic mm0-stuff and then Mephistolus will take over from there (we will have duplicate efforts because, I'm pretty sure that you are doing wonderfull stuff in mm0-hs... but though Mephistolus can rely on the mm0/mmu specification, it cannot rely on an externa > > 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] <javascript:>. >> 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/ccac3066-2155-4307-93b9-9743c98ee23d%40googlegroups.com.
