2012-04-21 11 views
21

Jaki jest najlepszy sposób, aby dowiedzieć się, co powoduje nierozwiązane meta? Czy istnieje sposób na przekształcenie wszystkich nierozwiązanych metas (i tylko nierozwiązanych) w dziury, poprzez rozwinięcie wszystkich otaczających symboli wieloznacznych, które można rozwiązać?Dowiedz się, które meta nie zostały rozwiązane w programie Agda.

Jeśli nic więcej, zmienianie nierozwiązanej mety w dziurę sprawi, że wiadomość o nierozwiązanej meta zniknie? Ponieważ wtedy myślę, że mogę spróbować zmienić każdy symbol wieloznaczny i każdy niejawny argument w dziury, aż wiadomość zniknie, a następnie dowiedzieć się, który z nich powoduje problemy ...

+0

Dodałem tag Haskell, ponieważ tag Agda ma tylko 17 pytań – sdcvvc

+1

w takim przypadku, pozwól mi zmienić także tytuł - jeśli przyjdziesz do tego pytania, myśląc, że to jest temat Haskell, będziesz się tylko mylić ... – Cactus

Odpowiedz

4

Jedno podejście (niekoniecznie najlepsze) to zastąpienie wszystkie ukryte argumenty za wyraźną podkreślenia:

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

Ta odpowiedź jest z listy mailingowej Agda: https://lists.chalmers.se/pipermail/agda/2012/004123.html

+0

Czy to oznacza pozytywną odpowiedź na moje pytanie z drugiego akapitu? "czy zmiana nierozwiązanej meta w dziurę sprawi, że wiadomość o nierozwiązanej meta zniknie?" – Cactus

Powiązane problemy