AZ
.\.\test.idr:18:1:
|
18 | add (a) (b) = (a + b, Refl)
| ^
unexpected "ad"
expecting dependent type signatureSize: a a a
2020 April 28
G
add : (a: Int) -> (b: Int) -> (c: Int, c >= a && c >= b)
add a b = (a + b, Refl)сделай отдельные леммы
AZ
Я не понимаю почему ошибка такая
G
Я не понимаю почему ошибка такая
из-за C: Int
AZ
Ладно завтра посмотрю. Спасибо
G
я опять поломал rustfmt
R
как вы это делаете вообще? такое ощущение, что вам что угодно дай, вы обязательно это поломаете. лул.
G
как вы это делаете вообще? такое ощущение, что вам что угодно дай, вы обязательно это поломаете. лул.
это так
S
почему хеш sha256-sdgjdflkgbsdsfklgnfsljlkgjfw46tsrkl называется SRI?
С
царь говорит он просто слабак
Царю отвечают, что он сам мудак
Т8
я опять поломал rustfmt
на плюсах написан, видать?
SS
Капеееец. Раст на Раст не похож
DF
Это Томака?
G
нет хирролот
G
я это сейчас пытаюсь макросами сгенерировать
G
чет макросы в расте реально неудобные
G
не чет совсем стрёмно
