История изменений
Исправление AndreyKl, (текущая версия) :
Т.е. в «искусственном случае» можно вызвать так (должно скомпиляться)
getType : (isInt : Bool) -> Type
getType False = String
getType True = Int
workingFunction : (x: Int) -> getType (x /= 42)
workingFunction 42 = "Мужик, это был смысл жизни, вселенной и всего такого!"
workingFunction x = x*2
main : IO ()
main = do putStr $ workingFunction 42
putStr $ "Квадрат 122 равен " ++ (workingFunction 122)
Исходная версия AndreyKl, :
Т.е. в «искусственном случае» можно вызвать так (должно скомпиляться)
getType : (isInt : Bool) -> Type
getType False = String
getType True = Int
workingFunction : (x: Int) -> getType (x == 42)
workingFunction 42 = "Мужик, это был смысл жизни, вселенной и всего такого!"
workingFunction x = x*2
main : IO ()
main = do putStr $ workingFunction 42
putStr $ "Квадрат 122 равен " ++ (workingFunction 122)