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