idris - Idris 中的常量

Question

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

myConstant : String
myConstant = "some_constant1"


myConstant2 : Int
myConstant2 = 123

如果是这样，在 REPL 中我在声明后得到一个异常:

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

Answer 1

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

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

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

或者有时 Idris 能够推断出类型:

Idris> :let myConstant = "some_constant1"

描述 here .