[Agda] Simple Agda Libraries
Wouter Swierstra
wss at Cs.Nott.AC.UK
Mon Jan 12 15:27:23 CET 2009
>> I have to admit I'm a bit hesitant to use the standard libraries. It
>> has a bit too much Unicode mixfix madness for my taste.
>
> Is it the use of non-ASCII characters which is problematic, or the use
> of mixfix operators?
A bit of both. There's nothing wrong with non-ASCII characters or
mixfix operators in principle, but its very easy to get carried away.
My goals are to find some set of modules that:
- are very modest and don't slow down load times too much;
- are reasonably uncontroversial;
- are useful - both for research and teaching.
I find that using the standard libraries tends to be overkill for a
lot of the small Agda developments I write. As other people might
share my experience, I reckoned it might make sense to bundle up some
mini-library that can spare us from having to define Nat and _+_ over
and over.
Wouter
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