[Agda] `reasoninig' example

Nils Anders Danielsson nad at chalmers.se
Tue Feb 26 11:12:41 CET 2013


On 2013-02-24 15:28, Serge D. Mechveliani wrote:
> Can anybody demonstrate, please, how can this be (approximately) rewritten
> by using EqReasoning, or may be, some other `reasoning' part of the
> library?

There are many examples of equational reasoning in the standard library.
You could for instance take a look at Algebra.Props.BooleanAlgebra.

-- 
/NAD


More information about the Agda mailing list