idris - 如何在 idris 中连接字符串和字符？

Question

我正在尝试连接一个字符串和一个字符以在 idris 中生成一个字符串。这是代码

*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
*Printf> 

我不明白这个错误。这里有什么问题？这是伊德里斯 1

标签： idris

Answer 1

检查类型！您正在尝试将两个字符串与++. 是否有该名称具有适当类型的函数？从错误中，您可以推断它++与类似列表的结构一起使用——这就是它提到的原因::；这可能与 的定义有关++，但类型检查器找不到该名称应用于字符串的函数。

缺少更具体的功能，需要解包字符串，连接末尾的字符，然后重新打包：

e3 = pack (unpack e1 ++ [e2])