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

它被描述爲here。

Answer 2

沒有在聲明全局常量特殊。你這樣做的方式是好的方法。

如果是這樣，在REPL我聲明後，得到一個異常：

伊德里斯的版本您使用的？在1.0上，對我來說一切正常。 你如何聲明變量？在文件中，而不是你在REPL中加載文件？