[Agda] stuck with "unsolved metas"

[Sergei Meshveliani]

On Wed, 2016-05-18 at 11:33 +0200, Andreas Abel wrote:
> On 17.05.2016 19:42, Sergei Meshveliani wrote:
> > Usually it helps adding implicit arguments. But not in this case:
> >
> >      debug =  implic (\ {p a b} → prime∣split {p} {a} {b})
> 
> You could try
> 
>    debug = \ {p a b} -> (implic (\ {p a b} → prime∣split {p} {a} {b})) 
> {p} {a} {b}
> 


Thank you. It works.
It also occurs that the inner "\ {p a b} " construct can be omitted, in
my example.

------
Sergei