[Agda] Agda standard library tutorial?

[Nils Anders Danielsson]

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

-- 
/NAD