[Agda] Q: Equational Reasoning

[Pierre-Evariste Dagand]

Hi,

> If there is a specific tutorial on how to do equational reasoning in Agda
> [...]

You can find some equational reasoning carried in Agda in:
"Algebra of Programming Using Dependent Types"
[http://portal.acm.org/citation.cfm?id=1428252]

This might go a little bit too far if you're looking for equational
reasoning only, though: the tutorial-ish Section actually derives an
implementation of 'sort' by squiggolistic black magic.

The paper and code are there:
[http://www.iis.sinica.edu.tw/~scm/2008/aopa/]


Hope this helps,

-- 
Pierre-Evariste DAGAND
http://perso.eleves.bretagne.ens-cachan.fr/~dagand/