Quel est un moyen idiomatique de définir ce que nous appelons une constante dans d'autres langues dans Idris? Est-ce cela?Constantes dans Idris
myConstant : String
myConstant = "some_constant1"
myConstant2 : Int
myConstant2 = 123
Si oui, REPL je reçois une exception après la déclaration:
(input):1:13: error: expected: "$",
Oui, c'est une façon idiomatique de définir des constantes dans Idris (dans les fichiers sources).
Toutefois, lorsque la liaison d'un nom dans REPL, vous devez utiliser la directive :let avec annotations de type explicites comme celui-ci:
Idris> :let myConstant : String; myConstant = "some_constant1"
ou parfois Idris est en mesure de déduire le type:
Idris> :let myConstant = "some_constant1"
Il est décrit here.
Rien de spécial à déclarer des constantes globales. La façon dont vous le faites est la bonne façon.
Si oui, REPL je reçois une exception après la déclaration:
Quelle version de Idris vous utilisez? Sur 1.0 tout fonctionne bien pour moi. Comment déclarez-vous des variables? Dans le fichier et que vous chargez le fichier dans REPL?
'Idris version 1.0'. Je le déclare en repl directement – Jodimoro