[Agda] Re: Accessing fields of algebra records

[Jacques Carette]

On 15-03-10 09:37 AM, N. Raghavendra wrote:
> At 2015-03-10T14:16:04+01:00, Nils Anders Danielsson wrote:
>
>> One can use "Module contents" (C-c C-o) to find out what a given module
>> exports.
> Thanks!  Did so just now, and as far as I can see, Data.Nat.Properties
> doesn't export any identity element or proof.

Look in Data.Nat.Properties.Simple.  Lots of useful proofs there, no 
matter how 'simple' they are!

Jacques