[opentheory-users] quoted strings

[Joe Hurd]

Hi Ramana,

If you stick to the *representation* of names that I suggest, with the
slashes left in, you will get the right properties of name equality.
Any representation that gives you the same equality property is fine
with me: indeed, OpenTheory uses a different one based on lists of
strings.

Removing slashes, so that

A\.b

and

A.b

have the same representation, will give you the wrong equality
relation on names, so beware.

Cheers,

Joe

On Mon, Jan 10, 2011 at 11:58 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> On Mon, Jan 10, 2011 at 7:37 PM, Joe Hurd <joe at gilith.com> wrote:
>> Hi Ramana,
>>
>>> First of all, what does it mean to obtain a string by matching a
>>> regular expression?
>>
>> Good question: I've tightened up the language to
>>
>> "A name command is a string that matches the following regular expression:"
>>
>>> And then you're left with the string, you discard the quotes, but what
>>> about the slashes inside the string?
>>
>> You leave the slashes in the string. The most important property here
>
> Leave the slashes in the string?
> But bool.art uses Data.Bool./\\, but I think the intention is for the
> name to be Data.Bool./\, no?
> I'm at the moment using String.fromString on the line I get back from
> TextIO.inputLine - I can't keep track of where all these functions
> (including whatever's printing things out to my terminal) add and
> remove slashes. Would you expect to have to use fromString on a line
> from an article, or should the line itself be right?
> If the extra slash in bool.art is wrong, perhaps you got caught by an
> SML printer that was trying to print something it could read back in
> to a value.
>
>> is that equality of names is the same as equality of the strings
>> representing them. For example, the two names
>>
>> A.b
>>
>> and
>>
>> A\.b
>>
>> are different, so it is good that they are represented by different
>> strings (because the slashes are left in).
>>
>> This is all that automatic tools for processing articles need to know.
>> However, for the purpose of displaying names in human-readable form,
>> the names might undergo some further processing, so A.b is actually
>> treated as the name b in the namespace A, and A\.b is treated as the
>> name A\.b in the global namespace, and as a result "show" tags might
>> transform them differently.
>>
>> In my eyes an import tool falls into the "automatic tools" category,
>> so I don't think you need to worry about the human readability angle.
>>
>> Does that help?
>>
>> Cheers,
>>
>> Joe
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>