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/d8062893-cdad-41fd-b348-33445386c408n%40googlegroups.com.
