[Agda] Agda standard library tutorial?

[Andreas Abel]

Hi Nisse,

thanks for telling me about this Module contents command, I did not know 
this and I guess it solves my main issue.

More tutorials like README.Nat would be VERY useful!!

One way of documenting the std.lib. would be to add user contributions 
that use the std.lib. to the std.lib. package.  Then you could start 
reading the contributions, see how people do stuff and mimick it.  This 
is a bit like the Coq maintained contributions.  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.

Cheers,
Andreas

On 1/13/11 6:41 PM, Nils Anders Danielsson wrote:
> On 2011-01-13 15:03, Andreas Abel wrote:
>> I must confess at this point I am lost. What the h... are all these
>> local modules and record and how on earth shall I quickly extract from
>> this heap what the names of the innocent lemmata are I want to use??
>
> I have been rather careful to reexport things (open public), so you can
> often project a large proportion of the fields from the top-level
> record. As you noticed the use of open public can make it hard to see
> what a module contains, so I implemented the "Module contents" command
> (C-c C-o), which can be used to see what a given module exports. In your
> case:
>
> module Test where
>
> open import Algebra
> import Data.Bool.Properties as BoolProp
>
> private
> module BCS = CommutativeSemiring BoolProp.commutativeSemiring-∨-∧
>
> Load Test and run the Module contents command for BCS. You get a rather
> long list which includes the lemma you mentioned:
>
> Modules
> Names
> _*_ : .Algebra.FunctionProperties.Core.Op₂ BCS.Carrier
> _+_ : .Algebra.FunctionProperties.Core.Op₂ BCS.Carrier
> _≈_ : .Relation.Binary.Core.Rel BCS.Carrier .Level.Level.zero
> [...]
> +-assoc : .Algebra.Structures.IsSemigroup._.Associative
> (.Algebra.Structures.IsCommutativeMonoid.isSemigroup
> (.Algebra.Structures.IsSemiringWithoutAnnihilatingZero.+-isCommutativeMonoid
>
> (.Algebra.Structures.IsSemiring.isSemiringWithoutAnnihilatingZero
> (.Algebra.Structures.IsCommutativeSemiring.isSemiring
> BCS.isCommutativeSemiring))))
> BCS._+_
> [...]
>
>> What can be done about this? I have some ideas, but cannot implement
>> them myself (otherwise I would not have this problem...)
>>
>> 1. Write a tutorial for the standard library that shows how its
>> definitions can be used. I know that there are README files, but
>> imho they only show how definitions can be used in principle, but
>> not concretely.
>>
>> 2. Supply (documented) example programs for each of the library
>> modules that explain how to use the stuff there. Would that not
>> also have the benefit to have some initial users and test cases?
>
> There is one mini-tutorial/example program, the module README.Nat. Is it
> useful? Would more modules like that one be of help to you?
>
>> 3. Provide "preludes" that extract the most important definitions from
>> a package into a single file, such that definitions are available
>> directly without sophisticated module- or open-statements. For
>> instance, one could have a Data.Bool.Prelude, Data.Nat.Prelude,
>> Data.List.Prelude etc.
>
> We have discussed this in the past, but no one has volunteered to do the
> work.
>
> http://thread.gmane.org/gmane.comp.lang.agda/634/focus=639
>