How do you define a non-generic recursive datatype in Idris?

Question

This is literally my first line of Idris code. When I looked up the documentation, all appeared proper:

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

This makes me think I may need to declare T to be a symbol in some fashion?

Answer 1

It works as expected inside an Idris source file. At the REPL however, declarations need to be prefixed with the :let command:

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

Thanks for the question. I learned something trying to answer it.