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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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