时间戳

首页 > 解决方案 > idris 中的纯关键字是否有特定的语法？

idris - idris 中的纯关键字是否有特定的语法？

问题描述

我正在开发一个函数来读取用户输入的列表，然后从中创建一棵树。这是代码

readList : IO (Maybe BSTree a)
readList = do x <- getLine
              if all isDigit (unpack input)
                  then do (_ ** xs) <- readList
                      pure ( listToTree (cast x)::xs )
                  else pure Nothing

这是 listToTree 的类型定义

listToTree : Ord a => List a -> BSTree a

pure ( listToTree (cast x)::xs )在对 readList 进行类型检查时，我在该行中收到“unexpected pure”错误。这是缩进问题吗？为什么不把纯关键字带到这里？

标签： idris

解决方案

使用 Idris 和类似语言工作时，缩进非常重要。我建议阅读一些标准库代码以了解缩进使用的约定。

以下将解析：

readList : IO (Maybe (BSTree a))
readList = do
  x <- getLine
  if all isDigit (unpack input)
  then do
    (_ ** xs) <- readList
    pure (listToTree (cast x) :: xs)
  else
    pure Nothing

推荐阅读