[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