B
а, а надо рантайм?
Size: a a a
2021 May 26
ΑZ
а идрис будет требовать чтобы ты перед тем как её вызывать проверил, что они равны. При этом число может быть рантаймовое
ΑZ
там с консоли считывается число если не заметил)
B
а, ну да
AN
а если сделать
:t b то что выведет?AN
или как там
ΑZ
Int
B
так стоп, Result<Nonzero<T>, Zero<T>>
TK
Интересно, что в рантайме неявно навешан предикат, исходя из ветви исполнения
TK
(или всё-таки в комптайме)
ΑZ
в компайл тайм
AN
if (x !== null) из тайпскрипта. Но там просто сахарок для конкретных кейсов.
Α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 b {contra}B
или читерство
AN
аа ну вот. а что такое contra?
ΑZ
Not (prf)AN
а я могу руками ее создать?
ΑZ
див у нас имеет вид
div : Int -> (b : Int) -> {auto p: Not (b = 0)} -> IntΑZ
можешь)
ΑZ
decEq это и делает