AZ
вывод типов не работает
в смысле? Это не задача вывода типов
Size: a a a
2020 June 06
G
Эм, так он же в школе ещё 😁
Да, летние каникулы
AZ
какой тип тут должен вывестись и не выводится?
DB
ну то есть ты ругаешь но даже не знашеь че ругаешь... Такое
Ну ругаю, потому что вывод типов мне важнее, чем конкатенация списков)
T1
Да, летние каникулы
скок лет?
p
в смысле? Это не задача вывода типов
а что по-твоему делает вывод типов? выводит типы. отсюда он не смог вывести тип.
G
вывод типов не работает
Это называется уже синтезис программ, а не вывод типов, AFAICT
p
значит не работает
DB
Ну ругаю, потому что вывод типов мне важнее, чем конкатенация списков)
А он на идрисе слабее.
G
скок лет?
15
AZ
а что по-твоему делает вывод типов? выводит типы. отсюда он не смог вывести тип.
какой тип он не вывел?
T1
оу, реально или рофл?
G
Реально
VS
Да, летние каникулы
Эхе, счастливые твои времена. Милота ты маленькая. Погуляли по паркам, поплавай лучше в это время :)
VS
Да, летние каникулы
Блять, таки да, вирус же
AZ
Переслано от Alex Zhukovsky
У меня такой вопрос, допустим я определил такой тип:
то оно будте иметь какие-то рантайм последствия по сравнению с
VarArgs : Type -> (numargs : Nat) -> Type
VarArgs t Z = t
VarArgs t (S k) = (next : t) -> VarArgs t k
И где-то пишуsum3 = VarArgs Int 3...
то оно будте иметь какие-то рантайм последствия по сравнению с
sum3Manual = Int -> Int -> Int -> Int?
AZ
Переслано от кана
по идее не должен, тип посчитается во время компиляции
AZ
Переслано от кана
в идрис2 вроде бы можно это явно указать чтобы не париться
VS
@hirrolot На мнгновение забыл про вирус