[Agda] Using Data.Sets

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Thu Nov 27 14:35:48 CET 2008


On 2008-11-25 08:06, J.Burton at brighton.ac.uk wrote:
> 
> The first place I looked for this information was the Sets module,
> could an example like this go in the comments?

In that case there are many modules which would need the same treatment;
many modules are parameterised.

> Or on the wiki/in the manual

Ulf's lecture notes from AFP08, which should be the first stop for
anyone trying to learn Agda (the wiki should probably point this out),
explain parameterised modules. Furthermore you can find out what a
"DecTotalOrder" is by following the hyperlink to its definition using
M-. (or the middle mouse button) in Emacs; a quick introduction to the
Emacs mode on the wiki would probably be in place.

Note also that patches to the library sources are welcome, and that the
wiki can be edited by anyone.

AIM 9 is currently in progress, and I hope that the wiki/documentation
will be in a (somewhat) better state after the meeting.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.



More information about the Agda mailing list