Подтвердить что ты не робот

Выяснение, какие метасы не решены в программе Agda

Какой лучший способ узнать, что вызывает нерешенные мета? Есть ли способ превратить все неразрешенные мета (и только неразрешенные) в дыры, расширив все окружающие подстановочные знаки, которые разрешимы?

Если ничего другого, изменит ли нераскрытую мета в отверстие, сообщение о нераскрытой мета исчезнет? Потому что тогда, я думаю, я могу попытаться изменить каждый подстановочный знак и каждый неявный аргумент в отверстия до тех пор, пока сообщение не исчезнет, ​​а затем выясните, какой из них вызывает проблемы...

4b9b3361

Ответ 1

Один подход (не обязательно лучший) заключается в замене всех неявных аргументы с явными символами подчеркивания:

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

Этот ответ из списка рассылки Agda: https://lists.chalmers.se/pipermail/agda/2012/004123.html