The problem with the “jumping” [-] button is fixed. I also added few more
features:
1) Adjustment of column widths: click a “three horizontal lines” button at
the top right corner of the proof table. Column widths are stored in the
local storage of the browser, so width adjustment may be
Thanks Benoit and Norm!
I will try to fix this behaviour of +/- button. (it happens in all browsers)
Best regards,
Igor
воскресенье, 20 декабря 2020 г. в 17:35:35 UTC+1, Norman Megill:
> On Sunday, December 20, 2020 at 11:13:33 AM UTC-5 Norman Megill wrote:
>
>> I like this very much. I
On Sunday, December 20, 2020 at 11:13:33 AM UTC-5 Norman Megill wrote:
> I like this very much. I think I will add a variable to the $t statement
> in set.mm so your base URL can be maintained there, instead of being
> hard-coded in metamath.exe. (And Thierry's structured version also, which
I like this very much. I think I will add a variable to the $t statement
in set.mm so your base URL can be maintained there, instead of being
hard-coded in metamath.exe. (And Thierry's structured version also, which
is currently hard-coded.) Give me a week or so.
An observation (in Chrome
That looks great. Congratulations!
Benoît
On Saturday, December 19, 2020 at 9:05:07 PM UTC+1 igori...@gmail.com wrote:
> Hello Norm,
>
> I’ve prepared a final version of my proof visualizations which you may add
> links to on the main site. URLs of pages have a form of
>
Hello Norm,
I’ve prepared a final version of my proof visualizations which you may add
links to on the main site. URLs of pages have a form of
https://expln.github.io/metamath/asrt/label.html Where “label” should be
replaced with the actual label of an assertion. (“asrt” stands for
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
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,
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
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
Norm wrote:
> Lest it be forgotten, another experiment that shows explicit substitutions is
> here::
> http://us.metamath.org/mpeuni/_mmbrows2p2e4.png
> This was done by Paul Chapman around 2007 I think.
> AFAIK this was just a proof of concept experiment, and he didn't publish the
> program
I like this. I think that showing explicit substitutions like this could
be very helpful to a beginner trying to learn how to follow Metamath proofs.
Lest it be forgotten, another experiment that shows explicit substitutions
is here::
http://us.metamath.org/mpeuni/_mmbrows2p2e4.png
This was
12 matches
Mail list logo
