[Agda] Re: Accessing fields of algebra records

Nils Anders Danielsson nad at cse.gu.se
Tue Mar 10 14:16:04 CET 2015


On 2015-03-10 14:11, Andrea Vezzosi wrote:
> Yeah, the "open public SubRecord subrecord" parts in the definitions
> of these records make this much better usable, however it seems the
> stdlib doesn't make this easy to discover.

One can use "Module contents" (C-c C-o) to find out what a given module
exports.

-- 
/NAD


More information about the Agda mailing list