[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