• programming У идриса какая-то проблема, если понимать что делаешь то можно вывести все доказательства показать пруфы и даже отрицания, и даже тоталити чеккер что-то разумное делает. Но если не понимать, то можно получить совершенно безумные доказательства, точнее выводы, хотя в разумном языке просто ничего не должно получаться. Надо будет потом попробовать агду затестить или даже сразу кок и посмотреть что во взрослых языках

Replies (3)