[Agda] Re: records and modules

[Ramana Kumar]

I figured out some of the answers myself.... details below

On Tue, Nov 22, 2011 at 12:20 PM, Ramana Kumar <rk436 at cam.ac.uk> wrote:
> I'm having trouble understanding the syntax for records, and how
> sometimes records seem to be treated as modules.
> I have a specific example below, and it may turn out that the problem
> is not just syntax.
>
> Suppose I have something like this:
>
> -----8<-----
> module Data.String where
> ...
> strictTotalOrder : StrictTotalOrder _ _ _
> ...
> -----8<-----
>
> Now in a separate module I try this
>
> -----8<-----
> open import Data.String renaming (strictTotalOrder to StringSTO)
> StringISTO = StrictTotalOrder.isStrictTotalOrder StringSTO
> S<-trans = IsStrictTotalOrder.trans StringISTO
> ...
> -----8<-----
>
> Firstly, the S<-trans line above is yellow, so something is wrong or
> missing, but I don't know what. Any idea?

I could remove the yellow by providing and repeating some implicit arguments:
S<-trans {i} {j} {k} = IsStrictTotalOrder.trans StringISTO {i} {j} {k}

Should these ought to be automatically inferred?

>
> Secondly, is there a simpler way to get the transitivity component for
> use in some proof later on?

I see now that StrictTotalOrder re-exports IsStrictTotalOrder, so I
don't have to open the nested record (and there are some notes on this
in the README for the standard library).

>