CODEWITHSUNDEEP
idris
bbarker
bbarker

Reputation: 13088

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

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?

Upvotes: 3

Views: 122

Answers (1)

Jeroen Noels
Jeroen Noels

Reputation: 351

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.

Upvotes: 4

Related Questions