I'm not so sure about that. It looks like the primary meaning of that
codepoint is "increment operator", used for small discrete changes, which
usually is an actual Delta (and read as such aloud). Visually, it also
shows the same typographic weight changes as is common with Delta that are
absent
You’re right! Actually, the code I used is x2206, which is listed as
“Symmetrical Difference”, so I believe it shall be the correct one.
https://codepoints.net/U+2206
This is a different code from Uppercase Delta (code x394), I wanted to describe
the shape - thanks for correcting me!
We can
On Sun, Apr 26, 2020 at 9:16 PM David A. Wheeler
wrote:
> I think formalization of ASCII is a cool idea, and I agree that
> '^' (and so on) would be *MUCH* better notation than _^ (and so on).
> If nothing else, the '...' notation is *widely* used to represent a single
> character,
> and we
I propose that we move symmetric difference into the main body
of set.mm. It's a well-known-enough operation, and technically
we now have two mathboxes that use it :-). It's not large.
The move should be easy; just move everything with the
symbol /_\ somewhere, say "Define basic set operations and
I think there is a unicode symbol for symmetric difference that is a white
upward pointing triangle (U+25B3 △), not an upper case Delta (which looks a
bit different due to weight changes along the glyph).
On Sun, Apr 26, 2020 at 8:19 PM Thierry Arnoux
wrote:
> Hi all,
>
> I've been aligning
Hi all,
I've been aligning also the "Structured Typesetting" pages with the ++
notation for concatenation and ∆ (Uppercase Greek Delta) for symmetrical
difference.
I also had to migrate the server on which those pages are hosted, the
pages are currently being regenerated, thanks for your
Heh, beat me by 5 seconds. Indeed, I meant 94.
On Sun, Apr 26, 2020 at 6:55 PM heiphohmia via Metamath <
metamath@googlegroups.com> wrote:
> Maybe this is just displaying my ignorance, but decimal 97 is ASCII 'a'.
> Perhaps you mean't 94, which corresponds to the caret (i.e. '^')?
>
> Mario
Maybe this is just displaying my ignorance, but decimal 97 is ASCII 'a'.
Perhaps you mean't 94, which corresponds to the caret (i.e. '^')?
Mario Carneiro wrote:
> > Use '^' in ASCII, frown in presentation: Alexander (prefers a symbol, not
> > "concat");
> >
>
> By the way, I would like to
> Use '^' in ASCII, frown in presentation: Alexander (prefers a symbol, not
> "concat");
>
By the way, I would like to reserve the notation '^' for the number 97, in
preparation for possible formalization of ASCII. (In MM0 I'm using _char
but 'char' is less likely to have overlapping usage.)
On Sun, Apr 26, 2020 at 17:31:09 +0200 (CEST) fl wrote:
> Dijkstra's argument doesn't seem to apply to our problem. He is dealing
> with finding a good convention to speak of a sequence of natural numbers
> using <= or <. It is not at all our problem. We don't use order relations
> to speak of a
Posted per FL's request
Norm
Forwarded Message
Subject: Dijkstra's argument
Date: Sun, 26 Apr 2020 17:31:09 +0200 (CEST)
From: fl
To: Megill Norman
Hi Norm,
can you post this.
Dijkstra's argument doesn't seem to apply to our problem. He is dealing
with finding a good
I'm going to pile on here. LIke Mario, Benoit, Alexander, and Dijkstra,
we should leave Word indexing as starting from 0.
It'd be a big change, with a lot of work, for no big benefit.
I haven't done a serious literature search, but I expect that the literature
will be inconsistent (just like it's
The comments on the concatentation symbol, in ASCII and in presentation,
were all over the place. The symbol choice is not a deal-breaker for people :-).
The (Unicode) presentation options came down to ++ or frown,
while the ASCII representations came down to ++, '^', or concat.
I think the
FWIW I agree with Benoit and Alexander (and Dijkstra) on both counts. :)
On Sun, Apr 26, 2020 at 4:23 AM Benoit wrote:
> Like Alexander, I agree that word indices start at 0... like natural
> numbers ;-)
>
> On Sunday, April 26, 2020 at 8:49:01 AM UTC+2, Alexander van der Vekens
> wrote:
>>
>>
Like Alexander, I agree that word indices start at 0... like natural
numbers ;-)
On Sunday, April 26, 2020 at 8:49:01 AM UTC+2, Alexander van der Vekens
wrote:
>
> About 0 or 1 as first (or zeroth ;-) ?) index of words (see remarks of FL
> and Norm below):
>
> Although there are good reasons
About 0 or 1 as first (or zeroth ;-) ?) index of words (see remarks of FL
and Norm below):
Although there are good reasons to index the symbols of a word W by 1 ..
length(W), there are also good reasons to start with 0. See, for example,
Wikipedia
16 matches
Mail list logo
