[Agda] stdlib for practical programming

[Sergei Meshveliani]

On Wed, 2013-09-25 at 19:36 +0300, Dmytro Starosud wrote:
> By "implicit parameters" do you mean {{instance}} parameters?
> 
> Thanks,
> Dima

Any arguments introduced as implicit.
(So far I never used {{...}} !).

Also I use `open' + `renaming' helps. For example:

  let open Ring R  using (Carrier; _+_; _*_; +comm; *assoc) 
      open Ring R' using () renaming (Carrier to C'; _+_ to _+'; 
                                                     _*_ to _*'_) 
  in
  a b : Carrier ...
  a + b  ... a * b  ...  +comm a b

  c d : C'
  ... c +' d ... c *' d

Here  R and R'  are the two instances of Ring made earlier.

Well, with the Haskell instances,  c +' d  can probably be replaced with
c + d,  because   a  and  c  come from different domains.

I wonder, can  Agda  arrange this?
When two instances of Ring are in scope, how to use the same symbol 
_+_ ?
Say,  +  is used for Nat and for  Nat \times Nat  in the same scope,
how to write the same symbol `+' ?

I ignored this questions because 
1) was satisfied with `renaming' (so far),
2) classes will still bring a hard problem of overlapping instances
   (such cannot be avoided in algebra). 
 

Regards,

------
Sergei