type signatures in interpreter

[ghost]

Currently, type signatures are not allowed in the interpreter. Instead, they lead to an error like in this example:

Idris> let list = ["foo","bar"] : List String in list
"(input)" (line 1, column 12):
unexpected reserved operator ":"
expecting "[", "if", "![", "?", "refl", "proof", "tactics", "case", operator, "(|", "[|", ")", ",", "**", identifier, "instance", "Integer", "Int", "Char", "Float", "String", "Ptr", float, natural, literal string, character, "Set", "()", "_|_", "_", "record", "\\", "let", "(", "|", "{" or "do"

This e.g. makes it impossible to define a list in a let-in-expression because the interpreter can't distinguish it from a vector.

[edwinb]

Try this instead:

Idris> let list : List String = ["foo", "bar"] in list

[ghost]

Ah, nice. Thanks :)