Re: [isabelle] about longer computation syntax sugar

Dear Liu Jian,

> When you simply change it as following, a error occurs.
>   range :: "index => seed => index => seed"
> where
>   "range k = (do
>      v <- range_aux (log 2147483561 k) 1;
>      if True return (v mod k) else return (v mod k)
>    done)"

The reason for this failure is the HOL if syntax: it demands a "then",
an in most cases has to be put in brackets:

>   "range k = (do
>      v <- range_aux (log 2147483561 k) 1;
>      (if True then return (v mod k) else return (v mod k))
>    done)"

> what's the meaning of following lines. Here, I can not understand the
> meaning of "CONST" and the difference between "=>" and "==" in a
> translation
> 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.

The difference between "=>" and "==" in first approximation is that "=>"
is only applied in input direction, whereas "==" is applied during input
and reversely during output.  For a detailed description on how the
syntax layer work I have to redirect you to the old Isabelle Reference
Manual which is
outdated in huge passages but the chapter on syntax still represents the
current implementation fairly well.

Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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