Re: [isabelle] lexical matters



I see.

Is there a printing mode for type-annotating constants and/or variables with
their types (like in HOL4)?  I'm concerned about the risk of statements
being displayed in a misleading way.

Mark

on 17/1/11 7:40 PM, Makarius <makarius at sketis.net> wrote:

> 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.