AZ
x и доказательство что x % 2 == 0? очень крутоSize: a a a
2020 March 25
В
Т.е. это функция которая принимает число
Но в расте такое даже пытаться накостылить нет смысла ибо это не будет рабоать с инфроструктурой
p
Да
S
И падение во время работы программы
ну пусть ошибку возвращает. Врядли idris предскажет, что введёт пользователь, там тоже такое может случиться, только не на уровне вызова функции, а на уровне преобразования из того, что ввел пользователь, в то, что хочет функция
SP
А что, нет? О.о
расскажи плз
G
тебе не могут false передать
AZ
module Main
infix 4 :+:
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(:+:) : a -> Vect k a -> Vect (S k) a
testFunc : (Vect n a) -> (Vect m a) -> (n = m) -> Integer
testFunc _ _ _ = 50
foo : Integer
foo = let arr = (1 :+: (2 :+: (3 :+: Nil)))
arrWithFour = 4 :+: arr
in testFunc arr arrWithFour Refl
main : IO ()
main = putStrLn "Hello world"
main = putStrLn "Hello world"AZ
вот например
AZ
попробуй запуститьь
G
module Main
infix 4 :+:
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(:+:) : a -> Vect k a -> Vect (S k) a
testFunc : (Vect n a) -> (Vect m a) -> (n = m) -> Integer
testFunc _ _ _ = 50
foo : Integer
foo = let arr = (1 :+: (2 :+: (3 :+: Nil)))
arrWithFour = 4 :+: arr
in testFunc arr arrWithFour Refl
main : IO ()
main = putStrLn "Hello world"
main = putStrLn "Hello world"Я тут
> не вижуAZ
Я тут
> не вижу(n = m)
p
расскажи плз
Ну в расте есть серде
G
(n = m)
Я про
> спрашивалAZ
ну напиши n > m, какая разница
AZ
тут любое условие может быть
G
ну напиши n > m, какая разница
У меня код не запустился, см. картинку сверху
p
ну пусть ошибку возвращает. Врядли idris предскажет, что введёт пользователь, там тоже такое может случиться, только не на уровне вызова функции, а на уровне преобразования из того, что ввел пользователь, в то, что хочет функция
Если Идрис не может доказать, оно просит тебя доказать
AZ
У меня код не запустился, см. картинку сверху
S
Если Идрис не может доказать, оно просит тебя доказать
то есть ввод там вообще не предусмотрен? Или я должен знать и доказать, что пользователь введет?
G
Если Идрис не может доказать, оно просит тебя доказать
Всё равно самому доказывать, Идрис может только по Ctrl+Alt+S поиск выражения делать