Re: [isabelle] Formal comments within inner syntax

Hi Florian,

Your suggestion looks very much like JavaDoc comments. However, I am less interested in formally checking that every parameter is documented rather than formally checking the documentation. So your suggested approach provides only little over what is currently available without the antiquotations @{spec} and @{arg}. In particular, the problem of
linking the parameter positions and types remains.

Do you have any idea how one could escape from inner syntax to the language context "document"?


On 10/09/14 10:28, Florian Haftmann wrote:
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,

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