:t (Nat -> Nat)

[danielwaterworth]

I get this error when I try to execute the above:

INTERNAL ERROR: "{A0} is not a Set"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues

I'm not sure if this is already covered by any of the other open issues.

[edwinb]

This is related to issue #32, namely that because elaboration of terms is type directed, the REPL is not very good at elaborating terms with binders like this and just gives up with an unhelpful message. Though there are a few ways I can try to fix this - I'll give it a go when I get a quiet moment.

For now you can say something like: let x : Set = Nat -> Nat in x which is ugly but works.

[danielwaterworth]

Thanks, that was quick.

[edwinb]

This is now fixed