ΑZ
если вопрос "могу ли я его создать не посмотрев на b" - можешь попробовать :)
Size: a a a
2021 May 26
B
вспомнил крестовые кнтракты, которые уже лет 10 обкщают
AN
да вопрос в этом.
TK
Или Option<NonZeroU32>. Но прикол в том, что делить на u32 всё равно можно. И даже пусть нельзя, типы-то разные выходят во втором случае. И доказательств не будет, что NonZero и правда не ноль содержит.
ΑZ
ну у тебя не выйдет ничего короче. Это примерно как в расте попробовать написать
fn foo<T>(t: T) -> T не использовав аргументΑZ
максимум панику сможешь сделать
AN
подожди но как decEq реализован?
TK
Проблема боттома, который вообще везде
AN
или это билт-ин штука?
ΑZ
это интерфейс которйы ты для своих типов реализуешь
TK
decEq : DecEq t => (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
П
А их вроде завезли же
B
из того шо нашел
AN
(b = 0) это что за сахар? это какая то на уровне типов конструкция?
B
нет, страус отклонил
П
:c Ашо почему
ΑZ
это тип
= с двумя генерик аргументамиAN
Т.е. у нас есть тайп конструктор '=', который принимает два типа