SP
но было бы прикольно
Size: a a a
2020 June 09
AZ
думал тайпскрипт уже догадался что там может быть nan
Он знает что в общем случае может прийти что то вроде nan
e
думал тайпскрипт уже догадался что там может быть nan
тока с чем ты его сравнивать собрался
SP
да причем тут это
e
а причем тогда заявление про nan
EG
Idris> 3
3 : Integer
Idris> 3 - 0
3 : Nat
Что происходит с тайп инференсом?
EG
3 + 0 опять даёт Integere
Idris> 3
3 : Integer
Idris> 3 - 0
3 : Nat
Что происходит с тайп инференсом?
тут не все идрис знают, почему в идрис чатике не спросишь
SP
а причем тогда заявление про nan
при том что в моей мировозрении number это такое где нет nan
EG
Потому что вопрос тупой, а Idris Beginners нету
e
при том что в моей мировозрении number это такое где нет nan
сделай свой number тип
С
при том что в моей мировозрении number это такое где нет nan
Так а какой это number? Целое? Или целое неотрицательное?
SP
Так а какой это number? Целое? Или целое неотрицательное?
ну обычный жсный намбер
С
Насколько я понимаю, корень из -1 будет давать NaN
SP
в расте тоже есть nan. какое же дно лол
SP
Насколько я понимаю, корень из -1 будет давать NaN
ну типом это надо делать же, ну епта
С
ну типом это надо делать же, ну епта
Я думаю, что тут возникнут НЕКОТОРЫЕ сложности
С
В духе известной картинки про "темку и накладочку"
EG
в расте тоже есть nan. какое же дно лол
nan есть везде
EG
Этого требует стандарт IEEE754