Re: [isabelle] lexical matters



On Mon, 17 Jan 2011, mark at proof-technologies.com wrote:

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?

As far as the kernel is concerned, the identity of atoms (variables, consts) consists of both the name and type, although "overloading" means something different in Isabelle.

In contrast, in the syntax layer (the so-called "term check/uncheck" phase, which generalizes the idea of type-inference) variables are expected to be consistently typed: equal name imples equal type, and scopes for variables vs. constants are resolved consistently.

If you print a term that violates this, it might look "funny", or outright misleading. This effect can already happen due to the customary omission of type information for variables.


Anyway, it also depends what is meant by "printed" exactly. In Isabelle there is quite a bit of extra formal markup in the output, that is not shown in plain text. In Proof General you already get the typical Isabelle color-code of blue/green/brown variables and black constants. In a Prover IDE like Isabelle/jEdit you could make even more out of that, e.g. tell the user the full truth about term atoms via tooltips or popups.


	Makarius





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