Re: [isabelle] about longer computation syntax sugar

On Mon, 1 Dec 2008, Florian Haftmann wrote:

> > translations
> >   "_do f" => "CONST run f"
> The "CONST" is a technical detail - for historical reasons, there are
> two syntactic classes of constants: constants which are represented with
> their proper qualified names in the syntax layer ("authentic constants")
> and constants which are represented just by their base name
> ("non-authentic constants").  New-style definition tools (definition,
> inductive, function, primrec with new "where"-syntax ...) yield
> authentic constants, whereas older devices do not (consts, constdefs,
> ...).  The "CONST" marker states that "run" is an authentic constant.

In fact, the CONST marker will always do the right thing, both for 
new-style constants with "authentic syntax" and the old-style ones.  But 
for authentic consts you cannot do it otherwise, while old-style 
non-authentic ones could be given as unqualified (and unchecked) base 
names, although this is not recommended.

In other words: always use explicit CONST if you refer to constants at the 
level of syntax translations.


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