AZ
Ты можешь написать
fn is_two x = x % 2 == 0
fn bar(x: i32{is_two x})юзай синатксис идриса
Size: a a a
2020 March 25
AZ
тогда больше людей поймут скорее всего
G
юзай синатксис идриса
В Idris есть типы с уточнением?
AZ
bar : (Int x) -> (x % 2 == 0) -> IO ()
bar x proof = ...p
юзай синатксис идриса
Я только 10 страниц из type development прочитал, толком до Идриса и не дошел
G
такое в расте не сделаешь.
+
p
bar : (Int x) -> (x % 2 == 0) -> IO ()
bar x proof = ...IO?
G
bar : (Int x) -> (x % 2 == 0) -> IO ()
bar x proof = ...А как выразить
x > 500?AZ
IO?
ну фукнция которая просто () возвращает немного бесполезная
AZ
А как выразить
x > 500?bar : (Int x) -> (x > 500) -> IO ()
bar x proof = ...p
ну фукнция которая просто () возвращает немного бесполезная
Так она должна bool возвращать
S
assert в геттере
AZ
Ты можешь написать
fn is_two x = x % 2 == 0
fn bar(x: i32{is_two x})функция bar у тебя ничего не возвращает
p
assert в геттере
И падение во время работы программы
G
bar : (Int x) -> (x > 500) -> IO ()
bar x proof = ...Но это при зависимом кейс-сплите будет просто True/False
В
bar : (Int x) -> (x % 2 == 0) -> IO ()
bar x proof = ...Т.е. это функция которая принимает число
x и доказательство что x % 2 == 0? очень крутоG
Т.е. это функция которая принимает число
x и доказательство что x % 2 == 0? очень крутоДа
p
функция bar у тебя ничего не возвращает
А, да. Но у меня в качестве пруфа вызывается функция foo
AZ
Но это при зависимом кейс-сплите будет просто True/False
тебе не могут false передать
AZ
в этом суть