这实际上是我的第一行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 是一个符号？
T
它在Idris源文件中按预期工作 . 但是，在REPL中，声明需要以 :let 命令为前缀：
:let
:let data T = Foo Bool | Bar (T -> T)
谢谢你的提问 . 我学到了一些试图回答它的东西 .
1 回答
它在Idris源文件中按预期工作 . 但是，在REPL中，声明需要以
:let命令为前缀：谢谢你的提问 . 我学到了一些试图回答它的东西 .