Most of the definitions don't need to be moved up, only the "structural"
ones that are required for actually defining the content of the new slot.
df-gsum is unfortunate because it is a relatively complex definition that
is also a dependency for the slot, but if you can write the slot without
any
On Thursday, February 13, 2020 at 5:46:36 PM UTC+1, Mario Carneiro wrote:
>
> That said, I think it would still be better to move all definitions needed
> for df-prds before it. This is a downside of the "everything structure"
> approach, but it does not displace too many definitions. We can
I realize that it seems especially inconvenient that moving df-gsum back
requires moving df-0g back too. But this better reflects the reality,
because df-gsum not allowed to refer to constants defined after cgsum
anyway (to prevent cycles), and placing df-gsum much further along just
makes this
> This is not a legal definition, this is mutual recursion which is not
> allowed. If you tried this in set.mm today you would get an error because
> mmj2 would not allow df-log to reference mulc. You would be forced to have
> an intermediate definition for the finite multiplication
On Tue, Jul 2, 2019 at 1:37 PM Benoit wrote:
> On Saturday, June 15, 2019 at 4:42:22 PM UTC+2, David A. Wheeler wrote:
>>
>> On Sat, 15 Jun 2019 07:05:43 -0400, Mario Carneiro
>> wrote:
>> > I would like to get away from label conventions in favor of something
>> > machine readable and not
On Saturday, June 15, 2019 at 4:42:22 PM UTC+2, David A. Wheeler wrote:
>
> On Sat, 15 Jun 2019 07:05:43 -0400, Mario Carneiro > wrote:
> > I would like to get away from label conventions in favor of something
> > machine readable and not hardcoded.
>
> I'm fine with adding additional
And also to vbe able to open définitions in mmj2.
The beautiful layout of the formulas designed by O'Cat complemented by the
colorization of variables realized by Mario Carneiro helps to read these
slightly esoteric formulas.
--
FL
--
You received this message because you are subscribed to
I also propose to put extensive textual description in commentaries to help
the
non-mathematically-oriented minds (in this respect df-prds should be
improved
for instance).
And also to add a link to a book that describes the concept. (The
description in
the book and the formal definition
On Tue, Jun 18, 2019 at 10:19 PM Norman Megill wrote:
> As presented to the public, Metamath is more than just a formal verifier.
> It is also an educational tool that presents the ZFC axioms and derives
> things from them. I think this is an important purpose. For certain
> technically-minded
On Sunday, June 16, 2019 at 1:35:04 AM UTC-4, Mario Carneiro wrote:
>
>
> I would like to renew my suggestion that we change these to ax-bi,
>>> ax-clab, ax-cleq, ax-clel. It adds complexity to the tooling to have an
>>> inconsistent naming convention, since we are signaling that these are
>>>
On Saturday, June 15, 2019 at 7:05:57 AM UTC-4, Mario Carneiro wrote:
Also the existing definition checker has hardcoded names all over the
> place, which has already caused problems on one occasion; adding a $j
> parser would fix this issue.
>
BTW if the checker is going to be rewritten, is
On Sat, 15 Jun 2019 07:05:43 -0400, Mario Carneiro wrote:
> I would like to get away from label conventions in favor of something
> machine readable and not hardcoded.
I'm fine with adding additional mechanisms.
However, I'd like to keep using & enforcing the label conventions.
I find they're
On Fri, Jun 14, 2019 at 10:15 AM 'Alexander van der Vekens' via Metamath <
metamath@googlegroups.com> wrote:
> Concerning the circular definitions: are there any meaningful cases, or
> even already examples in set.mm?
>
There are no circular definitions in set.mm. I was not clear, but the mmj2
13 matches
Mail list logo
