p
К тому же, что здесь и от чего зависит и в чём проблема с выражением этого на С++?
Я не знаю с++
Size: a a a
2020 July 18
Rn
В том, что числа только константные можно будет описать в C++ с такой функцией, а в Idris — и те числа, полученные в рантайме
так и в идрисе.
p
Если ты знаешь, то вырази пожалуйста
Rn
Я не знаю с++
ну на первую часть. Я не понимаю что ты хочешь?
p
По моим сведениям с++ не имеет завтипов
p
ну на первую часть. Я не понимаю что ты хочешь?
Вырази такую функцию в с++
H
так и в идрисе.
Не совсем, я могу с stdin считать число и пустить в такую функцию. В C++/Rust — нет
p
Чтобы она тайпчекалась
Rn
я не понимаю что я должен выражать
p
я не понимаю что я должен выражать
add1: n -> n + 1
add1 n = n + 1
add1 n = n + 1
Rn
Не совсем, я могу с stdin считать число и пустить в такую функцию. В C++/Rust — нет
ты не можешь этого сделать. Это так не работает
H
ты не можешь этого сделать. Это так не работает
А если я покажу пример, доказывающий такое поведение, ты согласишься?
p
ты не можешь этого сделать. Это так не работает
В идрисе так можно
KR
Хех, люблю наш оффтопик)
Rn
add1: n -> n + 1
add1 n = n + 1
add1 n = n + 1
ну, что конкретно ты хочешь? Т.е. что это значит в птушной системе типов.
Rn
В идрисе так можно
нельзя
p
В идрисе так можно
То что ты не знаешь что это возможно не говорит что это невозможно
Rn
То что ты не знаешь что это возможно не говорит что это невозможно
нет, у тебя проблемы с методичкой. Твоя система типов -1 порядка от моей
p
ну, что конкретно ты хочешь? Т.е. что это значит в птушной системе типов.
(n + 1) add1(int n);
Функцию с такой сигнатурой
Функцию с такой сигнатурой
Rn
поэтому в твоём пту это выражает однозначно, а в моей нет