[Agda] Re: Accessing fields of algebra records
N. Raghavendra
raghu at hri.res.in
Tue Mar 10 14:32:14 CET 2015
At 2015-03-10T14:11:07+01:00, 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.
>
> So in the first example you should be able to just write
> "CSR.identityˡ", or simply "identityˡ" if you "open CSR".
Thanks! I remember trying this earlier, and did so again now, but
1*n≡n : (n : ℕ) → 1 * n ≡ n
1*n≡n = CSR.identityˡ
where
module CSR = A.CommutativeSemiring NatProp.commutativeSemiring
gives the error
/Users/raghu/agda/My/SetTheory/Nat/IdentityElement.agda:22,9-22
Not in scope:
CSR.identityˡ
at /Users/raghu/agda/My/SetTheory/Nat/IdentityElement.agda:22,9-22
when scope checking CSR.identityˡ
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