2012-04-21 9 views
21

¿Cuál es la mejor manera de descubrir qué está causando las metas no resueltas? ¿Hay alguna forma de convertir todos los objetivos no resueltos (y solo los no resueltos) en agujeros, al expandir todos los comodines circundantes que se pueden resolver?Averiguar qué metas no están resueltas en un programa de Agda

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

+0

que añade una etiqueta Haskell, ya que la etiqueta Agda tiene sólo 17 preguntas – sdcvvc

+1

en ese caso, me deja cambiar el título también - si llega a esta pregunta pensando que se trata de Haskell, solo te confundirás ... – Cactus

Respuesta

4

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

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

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

+0

Entonces, ¿eso implica una respuesta positiva a mi pregunta del segundo párrafo? "¿cambiar un meta no resuelto en un hoyo hace que el mensaje sobre el meta no resuelto desaparezca?" – Cactus

Cuestiones relacionadas