[Agda] Q: Equational Reasoning

[Julien Oster]

On Mittwoch, 27. Mai 2009 15:17:40 Christoph Herrmann wrote:

Hello!

> thank you very much. I already guessed that the right way is by using
> the record hierarchy but how it has to be done is not so easy to
> see, even with the content of the example files. I have attached a
> working example based on your suggestions.

As far as I understood, your example is pretty much right, except that you 
usually "open" the records by treating them like parametrized modules, giving 
them the record instance you want to open them with.

So if you put the following before your definition of "foo":

open CommutativeSemiring commutativeSemiring hiding (_*_)

(note also that I left out the fully qualifying "Algebra." and 
"Data.Nat.Properties" in front of record and instance name, as you imported 
those modules with "open")

... you can just use the following in the definition:

...
 ≈⟨ *-comm m n ⟩
...

... and I guess that's pretty much what you want 8)

Regards,
Julien