[Agda] Proving a + suc b == b + suc a

[Serge D. Mechveliani]

On Thu, Nov 14, 2013 at 10:21:47AM +0100, Jan Stolarek wrote:
> Thanks Sergei! This looks more verbose, but it makes it clear what 
> derives from what. I like that. 
> As a beginner I'm only a bit scared of all these imports

Most of  `using ...'  parts can be omitted here, and  emacs  can show
the place in the corresponding module for each item clicked at in the
current source.

But I import items explicitly, because this makes a program more clear.
For example,  `setoid' and _+_  occur in many diferent library modules, 
and have many different meanings.

> - I didn't find any documentation or tutorial of the standard library 
> and learning it from the source comments seems like a daunting task.

Yes. After 17 months with Agda, I still ask sometimes 
"has Standard library such and such thing?".

1) I thank Agda people for answering to such.

2) For a beginner, it has sense to inspect (after, say, 2 months 
   experience) _all_ the Agda code of Standard library, paying attention 
   to signatures and skipping (for the first studying) most of 
   implementation. 

3) A regular documentation on the library is desirable, of a similar 
   kind as on the language 
   (a messy and boring work -- I agree).
   For example, look at the on-line doc on the Haskall-2010 Standard 
   library. 

Regards,

------
Sergei


> Dnia czwartek, 14 listopada 2013, napisa??e??:
> > open import Algebra  using (module CommutativeSemiring)
> > open import Data.Nat using (???; suc; _+_)
> > [..]