It is not hardcoded in mmj2, although it might be in the blacklist (which
gets out of date relatively quickly anyway and knows how to handle it).
Regarding the naming, I think it is a bit odd that a theorem called a1ii
does not use ax-1. Then again, idi doesn't use id either.
On Tue, Nov 10,
Likewise for me and nf.mm
> On Nov 10, 2020, at 6:29 PM, Jim Kingdon wrote:
>
> My answer is that iset.mm should do whatever set.mm does
>
>> On November 10, 2020 2:51:35 PM PST, Benoit wrote:
>> Hi all,
>>
>> I would like to relabel ~dummylink to ~a1ii, since it is the inference
>>
My answer is that iset.mm should do whatever set.mm does
On November 10, 2020 2:51:35 PM PST, Benoit wrote:
>Hi all,
>
>I would like to relabel ~dummylink to ~a1ii, since it is the inference
>associated with ~a1i (and "dummylink" is not the prettiest word).
>
>As Norm told me, this might have
Stephen Wolfram has been investigating dependencies between theorems,
including Metamath's set.mm, and has written up some findings here:
https://writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/
He mentions that ~syl is the most popular set.mm theorem (as
Hi all,
I would like to relabel ~dummylink to ~a1ii, since it is the inference
associated with ~a1i (and "dummylink" is not the prettiest word).
As Norm told me, this might have a few consequences, so I would need some
agreements before carrying on with the change:
* I would propagate this
Filip asked me to post the following:
Xpuzzle 1.2 has been released. New simple levels have been added, and a new
UI has been created. I think that would be a good practice environment for
Metamath newbies.
-- Filip
On Tuesday, September 1, 2020 at 6:18:22 PM UTC-4 Norman Megill wrote:
>
