Idris常数

Question

在Idris中，用什么惯用的方法来定义我们所称的常量？是这个吗？

myConstant : String
myConstant = "some_constant1"


myConstant2 : Int
myConstant2 = 123

如果是这样的话，在REPL中，声明后我会得到一个异常：

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

Answer 1

是的，这是在Idris中(在源文件中)定义常量的一种惯用方法。

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

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

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

Idris> :let myConstant = "some_constant1"

被描述为这里。

Answer 2

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

如果是这样的话，在REPL中，声明后我会得到一个异常：

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