[Agda] Newbie question, book exercise problem.

[Andreas Abel]

Nils Anders Danielsson a écrit :
> On 2009-11-29 19:18, Andreas Abel wrote:
>> The latter is greatly simplified by the module EqReasoning in the
>> standard library, if you know the right incantations to set it up,
>> like local module opening and on the spot module specialization...
>>
>>  .... where open Relation.Binary.EqReasoning (setoid (Vec _ _))
> 
> The propositional equality module contains a generalised, specialised
> instance of EqReasoning: ≡-Reasoning. See README.Nat for an example of
> its use:
> 
>  http://www.cs.nott.ac.uk/~nad/listings/lib/README.Nat.html

Thanks, Nisse, I was actually searching for it but did not find it.  I 
found the "Example use" in EqReasoning.agda.  Maybe this example could 
be extended to include the correct module import to make use of ≡-Reasoning.

Thanks!
Andreas


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/