[Agda] Re: Accessing fields of algebra records
N. Raghavendra
raghu at hri.res.in
Tue Mar 10 18:29:47 CET 2015
At 2015-03-10T18:05:04+01:00, Nils Anders Danielsson wrote:
> If you load up Algebra, then the command
>
> C-c C-o CommutativeSemiring RET
>
> should list both *-identity and +-identity.
Thanks! This is perfect! Now I can write
1*n≡n : (n : ℕ) → 1 * n ≡ n
1*n≡n = proj₁ CSR.*-identity
where
module CSR = CommutativeSemiring NatProp.commutativeSemiring
which is much simpler than what I did earlier.
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