Hey, I didn't say that was *all* it's for. It's not on the top of my list
of priorities, but I believe that the project will be in a good position to
formalize Godel's incompleteness theorem once the main goal is finished.
Already we have enough to formalize inductively defined structures like
> it is being used in order to define the input language of MM0 so that I can
> make a claim about an MM0 verifier
Ah, and here I had let my hopes get up that it was for formalizing Gödel's
Incompleteness Theorem (which is in the Metamath 100, after all).
On April 27, 2020 6:10:05 PM PDT,
On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote:
> >> I know, and this is a bigger issue for set.mm than in the mm0 databases
> >> because these are smaller and more purpose driven. One reason I went with
> >> _c notations for characters is because it is easier to read
> >> _h
On Tue, 28 Apr 2020 11:23:08 +0900, heiphohmia via Metamath
wrote:
> Norm, thank you for tagging v0.182 as well as merging the pull request.
> I am getting the impression that this thread has mostly increased your
> maintenance burden. That's really counter to my intent and needn't be the
>
Norm, thank you for tagging v0.182 as well as merging the pull request.
I am getting the impression that this thread has mostly increased your
maintenance burden. That's really counter to my intent and needn't be the case!
The whole release process on the GitHub side can be made very automatic.
On Mon, Apr 27, 2020 at 7:35 AM Norman Megill wrote:
> On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote:
> ...
>
>>
>> I know, and this is a bigger issue for set.mm than in the mm0 databases
>> because these are smaller and more purpose driven. One reason I went with
>> _c
Then U+25B3 (the current symbol) it is, for symmetry reasons (and to stay
away from alchemistry).
Benoît
On Monday, April 27, 2020 at 12:20:56 PM UTC+2, heiph...@wilsonb.com wrote:
>
> Well, U+2206 (INCREMENT) is the only correctly oriented triangle I see in
> the
> Mathematical Operators
> On Monday, April 27, 2020 at 3:11:43 AM UTC-4, heiphohmia wrote:
> ...
> >Previously, at the 0.181 update Giovanni asked you to incant the following:
> > git commit -m'Release version 0.181.'
> > git tag v0.181
> > git push
> > git push --tags
Yes, that will work just fine
Posted per FL's request.
Forwarded Message
Subject: Scheffer stroke
Date: Mon, 27 Apr 2020 19:21:36 +0200 (CEST)
From: fl
To: Megill Norman
Hi Norm,
can you post this:
In the commentary it is saïd that it is Russel and Whitehead who discovered
that NAND can be used as the
On Monday, April 27, 2020 at 3:11:43 AM UTC-4, heiphohmia wrote:
...
>Previously, at the 0.181 update Giovanni asked you to incant the
following:
>
> git commit -m'Release version 0.181.'
> git tag v0.181
> git push
> git push --tags
>
> It looks like this automatically
metamath-program.zip has never been on the home page. It was originally
added so Travis could download just the program without being slowed down
by unnecessarily including the .mm files, and it is still used for that.
Later it also become used for Linux distribution, and the compiled Windows
On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote:
...
>
> I know, and this is a bigger issue for set.mm than in the mm0 databases
> because these are smaller and more purpose driven. One reason I went with
> _c notations for characters is because it is easier to read
>
> _h
The us2 server may or may not go offline today because of maintenance on
the utility lines.
Norm
--
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
Well, U+2206 (INCREMENT) is the only correctly oriented triangle I see in the
Mathematical Operators block (https://codepoints.net/mathematical_operators).
The U+25B3 (WHITE UP-POINTING TRIANGE) is part of the Geometric Shapes block
(https://codepoints.net/geometric_shapes).
Looking at the
See also this page:
https://www.unicode.org/charts/nameslist/n_2200.html
I agree we shall exclude the uppercase Delta, so we are left with x2206 and
x25B3 as alternatives.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this
I proposed the symbol for symmetric difference in
https://github.com/metamath/set.mm/pull/1613#issuecomment-619592865 ,
namely U+25B3, after a quick google search for "unicode triangle". On the
html pages, it looks a bit too large (ideally, it should be the same size
as for \cap and \cup,
Hello Norm,
This is in reply to
https://groups.google.com/forum/#!searchin/metamath/Packaging$20Metamath$20for$20Linux%7Csort:date/metamath/z2kKJYgnz-g/xmRVy0KhCQAJ
For whatever reason my direct replies to the above seem to be falling into
Google's black hole, so I am sending this as a new
FWIW, this Wikipedia list corresponds TeX's \triangle with U+2206:
https://en.wikipedia.org/wiki/List_of_mathematical_symbols_by_subject
Mario Carneiro wrote:
> I'm not so sure about that. It looks like the primary meaning of that
> codepoint is "increment operator", used for small discrete
18 matches
Mail list logo
