[Agda] Re: Accessing fields of algebra records

[N. Raghavendra]

At 2015-03-10T10:39:20+05:30, N. Raghavendra wrote:

> Hi,
>
> How do I access the inner fields of complex records, e.g., the
> multiplicative identity of a commutative semiring?  If I write this:
>
> 1*n≡n : (n : ℕ) → 1 * n ≡ n
> 1*n≡n = CSR.isCommutativeSemiring.*-isCommutativeMonoid.identityˡ
>   where
>     module CSR = CommutativeSemiring Data.Nat.Properties.commutativeSemiring
>
> I get an error.
>
> Thanks and cheers,
> Raghu.

After looking at the records tutorial, I've found that this works:

1*n≡n : (n : ℕ) → 1 * n ≡ n
1*n≡n = identityˡ
  where
    open IsCommutativeMonoid
      (CommutativeSemiring.*-isCommutativeMonoid NatProp.commutativeSemiring)

but don't know whether this is the best way.

Cheers,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/