[Agda] Agda standard library tutorial?

[Andreas Abel]

This is not about maintaining every Agda code in the world; it is to 
have a set of meaningful maintained examples from which one can learn 
Agda and the use of the std.lib.

We are already maintaining a large amount of Agda code: the std.lib., 
and it is "other people's code", for the most of us.  So I do not see 
why we should not maintain examples as well.

Cheers,
Andreas

On 1/13/11 7:08 PM, Nils Anders Danielsson wrote:
> On 2011-01-13 18:57, Andreas Abel wrote:
>> More tutorials like README.Nat would be VERY useful!!
>
> Then we just need to find someone with the time and inclination to write
> them. :)
>
>> One way of documenting the std.lib. would be to add user contributions
>> that use the std.lib. to the std.lib. package.
>
> I want to make the standard library smaller, not larger, and I don't
> want to maintain other people's code.
>
>> An added benefit would be for users having done larger developments to
>> have them kept up to date with changes in Agda and the library; and
>> the developers would have a large regression test suite.
>
> If we had something resembling Cabal for Agda, then one could specify
> accurate dependencies for every package.
>