Re: [isabelle] treatment of qualified names in local theories



On Thu, Jun 30, 2011 at 6:45 AM, Makarius <makarius at sketis.net> wrote:
> On Wed, 29 Jun 2011, Brian Huffman wrote:
>> data MyBool = MyBool Bool
>>
>> I want to add qualifiers to distinguish these in Isabelle, something like
>> "type.MyBool" and "term.MyBool".
>
> It is probably easier to avoid this clash by using the conventional Isabelle
> naming scheme in such situations: terms are called "foo", types are called
> "foo_type".  A suffix will always be orthogonal to name spaces prefixes and
> qualifiers.
>
> If you do not want to present it like that to the end user, you can
> additionally augment the global const name space afterwards using
> Sign.const_alias etc. -- this looks to be the least intrusive workaround at
> the moment.

Thanks for the suggestion; I will have a closer look at the alias
operations on name spaces. My original plan was to maintain separate
name_space values for my embedded types and terms, with syntax rules
that would select the appropriate one based on context (similar to the
system currently used for parsing/printing Isabelle type expressions).
However, I was under the (mistaken) impression that
Name_Space.intern/extern were only able to fill in/hide qualifiers; I
didn't know about the support for aliases. It looks like I should be
able to use aliases with name suffixes to get everything to work with
local theories.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.