Constants in Idris

Question

What's an idiomatic way to define what we call a constant in other languages in Idris? Is it this?

myConstant : String
myConstant = "some_constant1"


myConstant2 : Int
myConstant2 = 123

If so, in REPL I get an exception after declaration:

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

Answer 1

Yes, it is an idiomatic way of defining constants in Idris (in source files).

However, when binding a name in REPL, you need to use the :let directive with explicit type annotations like this:

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

or sometimes Idris is able to infer the type:

Idris> :let myConstant = "some_constant1"

It is described here.

Answer 2

Nothing special in declaring global constants. The way you do it is the ok way.

If so, in REPL I get an exception after declaration:

Which version of Idris are you using? On 1.0 everything works fine for me. How do you declare variables? In file and than you're loading file in REPL?