Re: [isabelle] Formal comments within inner syntax

> 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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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