idris - 如何在 Idris 中定义非泛型递归数据类型？

Question

这实际上是我的第一行 Idris 代码。当我查阅文档时，一切都显得正确:

Idris> data T = Foo Bool | Bar (T -> T)
(input):1:6:
  |
1 | data T = Foo Bool | Bar (T -> T)
  |      ^
unexpected reserved data
expecting dependent type signature

这让我觉得我可能需要将 T 声明为某种形式的符号？

Answer 1

它在 Idris 源文件中按预期工作。然而，在 REPL 中，声明需要以 :let 命令为前缀:

:let data T = Foo Bool | Bar (T -> T)

感谢您的提问。我在尝试回答它时学到了一些东西。