How to concat a string and a char in idris?

[Ashwin Bhaskar]

Hi,

Why doesn't this work?

*Printf> :let e1 : String = "123"

*Printf> :let e2 : Char = 'f'
*Printf> :let e3 : String = e1 ++ pack [e2]
(input):1:9: When checking type of e3:
Can't disambiguate name: Prelude.List.::, Prelude.Stream.::, Data.Vect.::

(input):1:9:No type declaration for e3

Regards

Ashwin

[alru...@gmail.com]

Despite the apparent convenience,

:let e1 : String = "123"

does not define variable e1 to have type String. Variable e1 has type String = "123", which though rather nonsensical, is a valid Idris type.

At the repl, you can

:let e1: String

:let e1 = "123"

to get the desired behavior.