CODEWITHSUNDEEP
idris
Jodimoro
Jodimoro

Reputation: 4725

Constants in Idris

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: "$",

Upvotes: 4

Views: 183

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15404

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.

Upvotes: 7

Shersh
Shersh

Reputation: 9169

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?

Upvotes: 1

Related Questions