2012-04-21 12 views
21

Qual è il modo migliore per scoprire cosa causa i metas non risolti? C'è un modo per trasformare tutti i meta irrisolti (e solo quelli irrisolti) in buchi, espandendo tutti i caratteri jolly circostanti che sono risolvibili?Scoprire quali metas sono irrisolti in un programma Agda

Se non altro, trasformare un meta irrisolto in un buco fa sparire il messaggio sul meta irrisolto? Perché quindi credo di poter provare a cambiare ogni carattere jolly e ogni argomento implicito in buchi finché il messaggio non scompare e poi capire quale causa i problemi ...

+0

ho aggiunto un tag Haskell, dal momento che il tag Agda ha solo 17 domande – sdcvvc

+1

in tal caso, mi permetta di cambiamento il titolo pure - se vieni a questa domanda pensando che sia Haskell, ti sentirai solo confuso ... – Cactus

risposta

4

Un approccio (non necessariamente il migliore) è quello di sostituire tutte le implicite argomenti con sottolineature espliciti:

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

Questa risposta è dalla mailing list Agda: https://lists.chalmers.se/pipermail/agda/2012/004123.html

+0

Quindi ciò implica una risposta positiva alla mia domanda dal secondo paragrafo? "trasforma un meta irrisolto in un buco per far sparire il messaggio sul meta irrisolto?" – Cactus

Problemi correlati