Re: [isabelle] Formal comments within inner syntax

Hi Andreas,

> definition my_fun
>   :: "'a list         (* meaning of first parameter *)
>    => int             (* meaning of second parameter *)
>    => ('a, 'a list)"  (* description of results *)
> where ...
> Can such comments be made such that they are checked formally? Or does
> any of you have other convenient ways of documenting parameters and
> results of functions?

a radical answer would be to allow inner syntax to contain arbitrary
text cartouches ‹…› but I guess this would be a too massive change.

Alternatively you could devise a suitable set of antiquoations, e.g.

‹ at {spec "f xs k = ys"} …
 @{arg xs} …
 @{arg k} …
 @{arg ys} …

The disadvantage is that these can only follow the specification an
question.  But it will still leave the freedom to skip the Isar
specification totally and antiquote the specification theorems
explicitly, e.g.

‹ at {spec "f xs k = ys"} …
 @{arg xs} …
 @{arg k} …
 @{arg ys} …
 @{thms f.simps}

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.