Re: [isabelle] Formal comments within inner syntax



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

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

Well, my idea was that additional checks behind the back ensure the
@{arg …}s appear in the right order and completely.
I see, this indeed ensures a correct link, the link is still not as visible as with the
interleaved comments in Haskell.

Andreas




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