Idris中的常量

Question

在Idris中，定义常量的惯用方法是什么？这样做可以吗？

myConstant : String
myConstant = "some_constant1"


myConstant2 : Int
myConstant2 = 123

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

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

- Jodimoro

Answer 1

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

然而，当在REPL中绑定一个名称时，您需要使用:let指令并显式地添加类型注释，如下所示：

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

有时候，Idris能够推断出类型：

Idris> :let myConstant = "some_constant1"

这里描述了如何添加let绑定。

- Anton Trunov

Answer 2

声明全局常量没有什么特别的。你所做的方式是正确的。

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

你使用的Idris版本是哪个？对我来说，1.0一切都正常工作。你如何声明变量？在文件中，然后在REPL中加载文件吗？

- Shersh

---

Idris版本1.0。我直接在REPL中声明它。 - Jodimoro