On Fri, 10 Apr 2020 03:33:42 -0700 (PDT), Thomas Brendan Leahy
wrote:
> I've deleted the proof itself, but to give you an idea, here's an HTML file
> I made.
...
I'm trying to recover your proof of aacllem. Even after a few renames
I can't *quite* make it work in mmj2.
Below is the proof in
On Fri, 10 Apr 2020 03:33:42 -0700 (PDT), Thomas Brendan Leahy
wrote:
> I've deleted the proof itself, but to give you an idea, here's an HTML file
> I made.
Unless you object, I'm going to retype that proof aacllem from the HTML,
submit it to set.mm, and give you credit. That looks like
On Fri, 24 Apr 2020 18:50:11 -0700, Mario Carneiro wrote:
> I like the idea of using ++ for concatenation, particularly in ascii
> notation, since I don't want to try to reproduce a frown symbol in ascii. I
> think the most common symbol for this is adjacency though.
I also have (mild)
I like the idea of using ++ for concatenation, particularly in ascii
notation, since I don't want to try to reproduce a frown symbol in ascii. I
think the most common symbol for this is adjacency though.
Mario
On Fri, Apr 24, 2020 at 6:19 PM Norman Megill wrote:
>
> 1. I have no strong opinion
> 1. I have no strong opinion on ++ vs. concat, except that "concat" seems
> more self-explanatory. "concat" occurs 373 times in set.mm, so ++ would
> save 1492 bytes in set.mm size.
>
>
I'll also mention that Tarski used a frown symbol for concatenation in his
1965 paper. His notation is
