[Agda] records and modules

[Ramana Kumar]

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?

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