Idris 中的常量

Question

在 Idris 中定义我们在其他语言中称为常量的惯用方法是什么？是这个吗？

myConstant : String
myConstant = "some_constant1"


myConstant2 : Int
myConstant2 = 123

如果是这样，在 REPL 中声明后出现异常：

 (input):1:13: error: expected: "$",

Answer 1

声明全局常量没有什么特别之处。你这样做的方式是好的。

If so, in REPL I get an exception after declaration:

您使用的是哪个版本的 Idris？在 1.0 上，一切对我来说都很好。 你如何声明变量？在文件中，而不是在 REPL 中加载文件？

Answer 2

是的，这是在 Idris 中（在源文件中）定义常量的惯用方式。

但是，在 REPL 中绑定名称时，您需要使用带有显式类型注释的 :let 指令，如下所示：

Idris> :let myConstant : String; myConstant = "some_constant1"

或者有时 Idris 能够推断类型：

Idris> :let myConstant = "some_constant1"

描述为here。