[Agda] Proving a + suc b == b + suc a
Serge D. Mechveliani
mechvel at botik.ru
Thu Nov 14 12:09:35 CET 2013
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
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
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
> Dnia czwartek, 14 listopada 2013, napisa??e??:
> > open import Algebra using (module CommutativeSemiring)
> > open import Data.Nat using (???; suc; _+_)
> > [..]
More information about the Agda