[Agda] difficult "unsolved metas"

[Nils Anders Danielsson]

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 = λ {x y} → eCong {x} {y}"?

-- 
/NAD