Excellent. So I just happened to stumble upon a nice method used to organize
related deductions. Much appreciated.
On Fri, Oct 25, 2019 at 06:24:40AM -0700, Jim Kingdon wrote:
> This is relatively common when people want related theorems to have the same
> hypothesis.
>
> If you look at set.mm,
Hello,
The names in the subject line tripped me up. Is this intentional?
In particular, looking at the proof 2p2e4, the first unification is
oveq1i.1=df-2, which is followed by it's parent eqtr4i.1=oveq2i. The mismatch
between the deduction name and its hypothesis name confused me for a bit.
Hello,
The names in the subject line tripped me up. Is this intentional?
In particular, looking at the proof 2p2e4, the first unification is
oveq1i.1=df-2, which is followed by it's parent eqtr4i.1=oveq2i. The mismatch
between the deduction name and its hypothesis name confused me for a bit.
Metamath Zero is #7 on "Hacker News" ( https://news.ycombinator.com/ ), a
widely-read aggregator. That's quite impressive. Congrats, Mario!
There's no discussion yet, but if there is it will be at:
https://news.ycombinator.com/item?id=21358674
--- David A. Wheeler
--
You received this
Hello,
The names in the subject line tripped me up. Is this intentional?
In particular, looking at the proof 2p2e4, the first unification is
oveq1i.1=df-2, which is followed by it's parent eqtr4i.1=oveq2i. The mismatch
between the deduction name and its hypothesis name confused me for a bit.
Hi Mario,
That's a very nicely written paper, that shows some impressive work! It
made me want to try and learn mm0. I'll have to digest your article more.
I found some typos after a first reading (maybe for some of them, it is
actually me misunderstanding the paper):
p.4b: \bar y \sharp \bar
This is relatively common when people want related theorems to have the
same hypothesis.
If you look at set.mm, you'll see that oveq1i.1 only appears once, but
in a ${ $} block which includes both oveq1i and oveq2i .
On 10/25/19 2:51 AM, heiphoh...@wilsonb.com wrote:
Hello,
The logical
Hello,
The logical hypothesis for theorem oveq2i has the same name as that for oveq1i.
This tripped me up, but is the naming intentional?
In particular, I was writing up my own proof of 2p2e4 when I noticed the clash.
In fact, the proof of 2p2e4 exhibits the same exact issue: the first
(repost because I mixed up the threads)
The Metamath Zero system description paper (submitted to CPP 2020) is now
available on arXiv: https://arxiv.org/abs/1910.10703 .
The main highlights of the paper for metamath users are a chapter on how
MM0 is different from metamath and the shortcomings
The Metamath Zero system description paper (submitted to CPP 2020) is now
available on arXiv: https://arxiv.org/abs/1910.10703 .
The main highlights of the paper for metamath users are a chapter on how
MM0 is different from metamath and the shortcomings that MM0 is trying to
address. There is
us2.metamath.org/ works for me now, too!
On Thursday, October 24, 2019 at 4:51:57 PM UTC+2, vvs wrote:
>
> Works fro me. It's just probably needs time to propagate through all DNS
> caches.
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To
11 matches
Mail list logo
