[Agda] difficult "unsolved metas"

[Serge D. Mechveliani]

On Fri, Feb 08, 2013 at 05:18:52PM +0100, Nils Anders Danielsson wrote:
> On 2013-02-07 17:45, Serge D. Mechveliani wrote:
> >"unsolved metas" is reported exactly for the line of  "cong = eCong"
> >in the final fragment of
> >   ...
> >   eTo : sub-Setoid ->c baseSetoid
> >   eTo = record{ _($)_ = fromSub     -- : subCarrier -> baseCarrier
> >               ; cong  = eCong  }
> >         where
> >         eCong : _=s_ =[ fromSub ]=> _\equiv_
> >         eCong {x} {y} x-=s-y  = ...
> 
> Does your code work if you write
> 
>   "cong = \lambda {x y} -> eCong {x} {y}"?


(I have changed the \lambda symbol in this citation).

Yes!
(at least, it compiles)

-- if only I import   =[ fromSub ]=>  
not from  Relation.Binary.Core   but from  Relation.Binary.Indexed.
I think the former import was wrong because, the definition of  ->c
uses the latter import.

Thank you very much.

There remains some doubt about where, in general, to recall of this 
\lambda trick. 

Regards,

------
Sergei