AZ
хотя в идрисе total как раз и нужен чтобы избавиться от этого ИЛИ, иначе на тайплевеле чек неразрешим
Size: a a a
2020 August 17
AZ
Только bottom ненасеоенныц тип поэтому пофиг
населенный
AZ
panic!() например производит значение типа !
p
panic!() например производит значение типа !
! Не может быть сконструировано по идеи
p
В этом же его суть
AZ
! Не может быть сконструировано по идеи
fn foo() -> ! {
exit(-1);
}AZ
fn foo2() -> ! {
loop {}
}p
fn foo() -> ! {
exit(-1);
}Ну и где ты тут конструируешь что-то?
r
panic!() например производит значение типа !
Произвести значение типа
! означает не производить никаких значенийAZ
Ну и где ты тут конструируешь что-то?
компилируется значит сконструировал
Т8
panic!() например производит значение типа !
void ?p
компилируется значит сконструировал
Не вижу связи
AZ
Не вижу связи
у
loop {} возвращаемое значение !p
у
loop {} возвращаемое значение !И?
AZ
значит используя loop {} я могу сконструировать значение типа !
AZ
Т-34 85
void ?Void в нормальных языках, да. Но не в сишке
p
у
loop {} возвращаемое значение !foo: Int -> Void
Тут по твоему сконструируется Void?
Тут по твоему сконструируется Void?
AZ
AZ
точнее не так
Т8
Это как? Как он может сконсируироваться? Какой размер?