Constants in Idris

Constants support character, string, boolean, and numeric values.

module Main

import Data.Pretty

const s : String
s = "constant"

main : IO ()
main = do
  putStrLn s

  let n : Integer
  n = 500000000

  let d : Double
  d = 3e20 / cast n

  putStrLn $ show d
  putStrLn $ show (cast d : Int)

  putStrLn $ show $ sin (cast n : Double)

To run the program, put the code in a file named constants.idr and use the Idris compiler to execute it:

$ idris constants.idr -o constants
$ ./constants
constant
6.0e+11
600000000000
-0.28470407323754404

Now that we can define and use constants in a basic Idris program, let’s learn more about the language.