伊德里斯的常数

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> :let myConstant = "some_constant1"

这里描述.