TK
Если b = 0, то на него нельзя делить, в противном случае можно, а проверка была сделана выше с decEq благодаря противоречию
Size: a a a
2021 May 26
B
не помню, но сказал нет
AN
да ты раньше ответил чем я дописал
AN
> decEq Here Here = Yes Refl
а я могу тут вставить мусор?
а я могу тут вставить мусор?
AN
decEq Here Here = No contra —I am bad
ΑZ
Ну тебе в No нужен пруф с контрпримером
TK
Не можешь, как и с обычными типами, пока не реализуешь интерфейс
TK
Да и потом, делить на мусор всё равно не получится
AN
хитро.
ΑZ
тот же Refl не просто так там
ΑZ
кажется что это юнит который ничего не прниимает
ΑZ
но это не так на самом деле
AN
для меня это просто набор букв)
AN
что оно делает?
ΑZ
рефлексивное равенство
B
только похоже ли оно на завтипы
ΑZ
короче надо книжку читать, там все очень интересно
AN
про идрис книжка?
ΑZ
это можно, да