Re: [isabelle] lexical matters



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Mark,

I think, I can answer that; other readers should feel free to correct me.

mark at proof-technologies.com 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.

> and, whether it is or not, what does
> the printer output?

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

- -Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFNMx6UczhznXSdWggRAnCrAJwLsrSrcYzqATD6GF2MxiRTJ9o/qgCfd8Uq
r24zX3C4KVZvEN3aqTAY4Ks=
=4xpw
-----END PGP SIGNATURE-----





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