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

[Mateusz Kowalczyk]

On 14/11/13 09:21, 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 - I didn't find any documentation or 
> tutorial of the standard library and learning it from the source comments seems like a daunting 
> task.
> 
> Janek

Unfortunately I don't think there is any overview of the standard
library and no documentation on what the modules do ‘in simple words’.
It's partially to be expected considering how generic such a library has
to be for a proof assistant but I agree that it sets a high bar for
beginners (such as myself).

I think that the way to learn about it at the moment is to look in the
module/at the module name, go study the topic it relates to and then
come back to the Agda code and try to match up what you learned with
what you see. While it doesn't sound too friendly, I think that you'll
need this knowledge anyway to use the modules in a meaningful way in
your proofs.

I do hope that one day some documentation will exist on using some of
the modules. Some entry-level guide ‘papers’ show how to use the
≡-Reasoning syntax but I haven't seen much help otherwise. If anyone
knows of such an overview, even incomplete, please post about it!

-- 
Mateusz K.