Yeah, that would be an honour for me to make a contribution to Metamath. Sure, I want to solve few technical issues, test them during some time and then you can add links.
I also thought regarding unicode symbols. I will spend some time to try to add possibility to show both ascii and unicode symbols (but I don't promise to do it fast enough because of lack of time :) ) Actually I've just figured out that I can use this feature of metamath.exe to verify what my program generates. This is not straightforward though but possible. I will write a message when I think this my visualisation is stable enough so we can start adding links. Best regards, Igor вторник, 8 декабря 2020 г. в 17:13:15 UTC+1, Norman Megill: > When this becomes stable, I can add a link to your version on each theorem > page of the main site, like the link that now says "Structured version" for > Thierry's pages. This will let you have direct control over your content. > (To start with, your base URL would be hard-coded in metamath.exe, but > later I can add a keyword to the $t statement in set.mm so the URL can be > maintained there.) > > I don't know your long term plans, but I'll mention that personally > (although I may be in the minority) I don't mind the ASCII notation in the > proofs. It shows a beginner the direct relationship to the set.mm source > and allows easy copy/paste. The user can also see the direct relationship > between the ASCII and the Unicode rendering by switching between your page > and the standard page, without having to consult set.mm or the awkward > "ASCII Symbol Equivalents" page. > > BTW although of course it's not as convenient as your pages, some people > might not know that metamath.exe can show the substitutions made in a step: > > MM> show proof 2p2e4 /detailed_step 18 > Proof step 18: eqtr4i.1=oveq2i $p |- ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ) > This step assigns source "oveq2i" ($p) to target "eqtr4i.1" ($e). The > source > assertion requires the hypotheses "cA" ($f, step 13), "cB" ($f, step 14), > "cC" > ($f, step 15), "cF" ($f, step 16), and "oveq1i.1" ($e, step 17). The > parent > assertion of the target hypothesis is "eqtr4i" ($p, step 47). > The source assertion before substitution was: > oveq2i $p |- ( C F A ) = ( C F B ) > The following substitutions were made to the source assertion: > Variable Substituted with > C 2 > F + > A 2 > B ( 1 + 1 ) > The target hypothesis before substitution was: > eqtr4i.1 $e |- A = B > The following substitutions were made to the target hypothesis: > Variable Substituted with > A ( 2 + 2 ) > B ( 2 + ( 1 + 1 ) ) > > Norm > > > On Tuesday, December 8, 2020 at 9:27:57 AM UTC-5 [email protected] wrote: > >> Norm, Jim, thanks for your feedback! >> >> I updated the proof visualisation - all steps are collapsed by default >> and a [+] button will expand selected node. Examples: >> http://metamath.d4-e5.de/v2/data/2p/2e/2p2e4.html >> http://metamath.d4-e5.de/v2/data/sq/rt/2i/sqrt2irr.html >> http://metamath.d4-e5.de/index.html >> >> Also offline version may be found here >> https://drive.google.com/drive/folders/1na2UM270rsCd85BQCmaJJSnak8HywfL8?usp=sharing >> (its >> size is 500M when unarchived). >> >> At the moment, step numbers in my proof visualisation don't correspond to >> step numbers on http://us.metamath.org in many cases. This is because of >> duplicate steps in my visualisation. I will fix this. >> >> Best regards, >> Igor >> >> вторник, 1 декабря 2020 г. в 03:22:00 UTC+1, [email protected]: >> >>> On 11/30/20 6:03 PM, Paul Chapman wrote: >>> >>> > I may be getting too old/lazy to code. Thirty years ago I’d’ve written >>> > a knockout replacement for mmj2. ;) >>> >>> Haha I'll let you be the judge of whether you are too old/lazy to code. >>> >>> But if you are just disinclined to shave all the yaks required to get a >>> smalltalk compatible with that experiment running again, hey that >>> strikes me as quite understandable quite aside from age. Quite a saga. >>> >>> >>> -- 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/feed3226-2399-43a5-9a62-9475d3e7f329n%40googlegroups.com.
