[Agda] beginner questions

[Nils Anders Danielsson]

On 2012-07-23 14:04, Serge D. Mechveliani wrote:
> (2) Do there exist papers (manustripts, descriptions, explanation) about
>      the Standard Library (somewhat its principles, architecture etc.) ?

The README contains some information:

   http://www.cse.chalmers.se/~nad/listings/lib-0.6/README.html

> (4) Instances in the Standard Library.
> The Standard Library lib-0.6 provides the `classes' (records) for
> Semigroup, Group, ..., Ring.
> Does it also provide some classical instances for them?
> For example,
> * the instances up to  CommutativeRing  for  Integer
>    (CommutativeSemigroup, CommutativeGroup  for  +,
>     CommutativeSemigroup, CommutativeMonoid for  *,
>     distributivity, CommutativeRing
>    ),

Yes. See README.Integer
(http://www.cse.chalmers.se/~nad/listings/lib-0.6/README.Integer.html)
for an example.

> * the instance (record map)
>    (Ring A, Ring B) => Ring (A, B) where  -- coordinatewise operations
>                                           -- in the direct product A x B

No, I don't think so.

> How could these instances (record maps) look?

See Relation.Binary.Product.Pointwise:

   http://www.cse.chalmers.se/~nad/listings/lib-0.6/Relation.Binary.Product.Pointwise.html

-- 
/NAD