Constants in Idris

Viewed 164

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