[Agda] Re: Accessing fields of algebra records
N. Raghavendra
raghu at hri.res.in
Tue Mar 10 18:43:01 CET 2015
At 2015-03-10T20:50:23+04:00, Sergei Meshveliani wrote:
> It could be simpler:
>
> CommutativeSemiring.identityˡ NatProp.commutativeSemiring
You're right. As Nils has pointed out, the CommutativeSemiring module
in Algebra exports *-identity, so one can just write
1*n≡n : (n : ℕ) → 1 * n ≡ n
1*n≡n = proj₁ $ CommutativeSemiring.*-identity NatProp.commutativeSemiring
Thanks and 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