[Agda] Simple Agda Libraries

[Nils Anders Danielsson]

On 2009-01-14 13:44, Shin-Cheng Mu wrote:

> Firstly, the Haskell Prelude contains most of what I need and
> I can start coding immediately

It would be easy to set up a prelude which reexports some commonly used
definitions:

   module Prelude where

   open import Data.Empty public

   import Data.Unit
   open Data.Unit public using (⊤; tt)
   module Unit where
     open Data.Unit public using (poset)

   import Data.Nat
   open Data.Nat public using (ℕ; zero; suc; _+_)
   module Nat where
     open Data.Nat public using (poset)

   -- Or something like that…

Contributions are welcome, as always.

Unfortunately Agda cannot bring two constructors with the same name into
scope at the same time when open public is used (unless they come from
the same module). I have raised a ticket for this:

   http://code.google.com/p/agda/issues/detail?id=124

> Secondly, I found it quite hard to dig through, for example,
>    ≤-trans = IsPreorder.trans (IsPartialOrder.isPreorder
>                                  (Poset.isPartialOrder poset))
> to extract transitivity of some datatype. Perhaps there is
> an easier way?

These record modules open the underlying records publicly, so you can
use

   ≤-trans = Poset.trans poset.

This is documented on the wiki page for the standard library:

   http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary

> One has got to be quite familiar with the Standard Lib
> to know where to find what one needs.

Yes. There is a short introduction to the library on the Agda wiki, but
a better overview would be nice.

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