ΑZ
и ты ег оможешь использовать например чтобы скормить функции div
Size: a a a
2021 May 26
AN
но каким образом?
ΑZ
все проверки генерируют пруфы. А дальше тайпчекер пытается найти в скоупе подходящие
s
Тыкни, а то я не могу найти.
AN
как появляются. т.е. у тебя какое то выражения "существует Y что x: S Y"?
ΑZ
runtimeDiv : IO ()
runtimeDiv = do
aStr <- getLine
let a = the Int (cast aStr)
bStr <- getLine
let b = the Int (cast aStr)
case decEq b 0 of
(Yes prf) => putStrLn "Cannot divide by zero"
(No contra) => print $ div a bAN
ой не помню. я так проклацал чисто и закрыл. Там какие то ссылки на конфу. Они прям на канале раста в ютубе еще есть.
ΑZ
ты вызываешь функцию "сгенерировать пруф", он и генерируется
ΑZ
например decEq генерирует Either (доказали, не доказали)
s
Если ты про Rust Verification Workshop 2021, то там всё не то.
AN
ага про это. ну не то так не то. жаль (
B
так а в чем проблема это на раст перевести
AN
ну и что это за тип такой? просто какой то синглетон про равенство нулю?
ΑZ
есть типа "равно"
ΑZ
когда какие-то вещи равны
ΑZ
есть общая функция dec (от decide) для проверки что утверждение верно
ΑZ
т.к. часто проверяется равенство для него есть хелпер decEq
ΑZ
не понял про какой синглтон речь
ΑZ
в том что единственный способ в расте написать это - конст генерики - не рабоатет для рантайм значений
ΑZ
раст будет требовать чтобы у тебя была константа чтобы провалидировать функу