haskell - keywords - Averiguar qué metas no están resueltas en un programa Agda

meta tags generator

Question

¿Cuál es la mejor manera de averiguar qué está causando metas sin resolver? ¿Hay una manera de convertir todos los metatos no resueltos (y solo los no resueltos) en agujeros, al expandir todos los comodines circundantes que se pueden resolver?

Si nada más, ¿cambiar un meta sin resolver en un agujero hace que el mensaje sobre el meta sin resolver desaparezca? Porque entonces supongo que puedo intentar cambiar cada comodín y cada argumento implícito en agujeros hasta que desaparezca el mensaje y luego averiguar cuál está causando los problemas ...

Answer 1

Un enfoque (no necesariamente el mejor) es reemplazar todos los argumentos implícitos con guiones bajos explícitos:

f {_} {_} {_} (x {_} {_} {_})

Esta respuesta proviene de la lista de correo de Agda: https://lists.chalmers.se/pipermail/agda/2012/004123.html