Re: [isabelle] lexical matters

Thanks for your answers, Matthias/Makarius.

I have a follow-up question...  What about variables overloaded with other
variables (i.e. same name but different type) or overloaded with constants
(same name, any type) - can terms with any such overloading be parsed, and
what happens when they are printed?


on 16/1/11 7:21 PM, Makarius <makarius at> wrote:

> On Sun, 16 Jan 2011, Matthias Schmalz wrote:
>> mark at schrieb:
>>> On a related topic, what does Isabelle do for parsing/printing
>>> irregular variable/constant names?  E.g. a variable with a space in its
>>> name.  Is it possible to parse such a variable name,
>> No, as
>> term "a a"
>> is rejected.
> By extending the syntax in user space, you can easily inject odd strings
> into the term language, e.g. via something like
> FREE ''foo bar''
> with a grammar production for the "FREE" literal token and a suitable
> parse translations.  See the existing CONST notation, although I do not
> really recommend to try this at home.
>> If you create variables with irregular names using the ML
>> infrastructure, the printer justs prints them:
>> ML_val {*
>> cterm_of @{theory} (Free ("a a", @{typ bool}))
>> *}
>> ... prints
>> val it = "a a" : cterm
> This use of cterm_of reminds me of an old trick that has come out of use
> some years ago, because printing with the background theory certificate
> lacks local syntax of the foreground context (local theory or proof body).
> Did you come up with idea yourself, or do we still have it in some old
> manual?
> Here is the localized version:
> ML_val {*
> writeln (Syntax.string_of_term @{context} (Free ("a a", @{typ bool})))
> *}
> Makarius

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