[Agda] stuck with "unsolved metas"

Andreas Abel abela at chalmers.se
Wed May 18 11:33:28 CEST 2016


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}

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/


More information about the Agda mailing list