[opentheory-users] quoted strings

[Ramana Kumar]

On Mon, Jan 10, 2011 at 9:08 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> So the OpenTheory name for conjunction really is Data.Bool./\\ then. All right.

It's consistent, but this has got to be wrong.

Let me try asking again, differently.

Consider http://opentheory.gilith.com/opentheory/packages/bool-def-and-1.0/bool-def-and-1.0.html.
The tool-tip for the defined constant suggests that its name is 'Data.Bool./\'.
(To be clear, I used quotes there to ensure I was referring to the
name and not to the constant; the name is between the quotes.)
Now if you download the theory package linked from that page and look
at the article file, line 1 is as follows.

"Data.Bool./\\"

(This time, the double quotes are part of the line; the blank lines
delimit my quotation of the line.)
Why are there two (back)slashes in the line?

The article format description doesn't say very much about names.
What I have gathered is that a name command is a string delimited by
double quotes, and the meaning of a name command is to push a name
object containing the string between the quotes onto the stack.
I took it as implied that the name object would contain the string
that is actually the name of some constant (or operator or variable)
so it can be used later in making a particular constant (etc.) object.
There's no indication that names are different from strings, although
maybe that's supposed to be obvious.
But more importantly, in that case, there's no description of the
relationship between names and the strings used in article files to
represent them.

>
> On Mon, Jan 10, 2011 at 9:02 PM, Joe Hurd <joe at gilith.com> wrote:
>> Hi Ramana,
>>
>>> Hmm... could I ask one more question actually, to be sure?
>>> You gave the example of the two names A\.b and and A.b.
>>> Suppose I have an article that defines two different constants with these names.
>>> Somewhere in the article file there must be lines that instruct the
>>> virtual machine to push those names onto the stack.
>>> What exactly would those lines look like?
>>
>> The two command lines would be
>>
>> "A\.b"
>>
>> and
>>
>> "A.b"
>>
>> Two *different* names pushed onto the stack.
>>
>> Cheers,
>>
>> Joe
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>