[Agda] Re: Accessing fields of algebra records

[Nils Anders Danielsson]

On 2015-03-10 14:37, 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.

If you load up Algebra, then the command

   C-c C-o CommutativeSemiring RET

should list both *-identity and +-identity.

-- 
/NAD