Idris 中的常量

【问题标题】：Constants in IdrisIdris 中的常量
【发布时间】：2017-10-20 23:11:55
【问题描述】：

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

myConstant : String
myConstant = "some_constant1"


myConstant2 : Int
myConstant2 = 123

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

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

【问题讨论】：

标签： idris

【解决方案1】：

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

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

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

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

Idris> :let myConstant = "some_constant1"

它被描述为here。

【讨论】：

【解决方案2】：

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

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

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

【讨论】：