[Agda] Re: Accessing fields of algebra records
N. Raghavendra
raghu at hri.res.in
Tue Mar 10 14:37:46 CET 2015
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.
Cheers,
Raghu.
--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/
More information about the Agda
mailing list