Values in Idris

import System.IO

main : IO ()
main = do
    -- Strings, which can be concatenated with ++
    putStrLn ("idris" ++ "lang")

    -- Integers and floats
    putStrLn $ "1+1 = " ++ show (1 + 1)
    putStrLn $ "7.0/3.0 = " ++ show (7.0 / 3.0)

    -- Booleans, with boolean operators as you'd expect
    putStrLn $ show (True && False)
    putStrLn $ show (True || False)
    putStrLn $ show (not True)

Idris has various value types including strings, integers, floats, booleans, etc. Here are a few basic examples.

Strings in Idris can be concatenated using the ++ operator.

Integers and floats work as expected. Note that in Idris, you need to use show to convert numbers to strings for printing.

Booleans in Idris work with the standard boolean operators. The not function is used for boolean negation.

To run this program, save it as values.idr and use the Idris interpreter:

$ idris values.idr -o values
$ ./values
idrislang
1+1 = 2
7.0/3.0 = 2.3333333333333335
False
True
False

In Idris, we first compile the program to an executable using idris, and then run the resulting executable.

Idris is a pure functional language with dependent types, which makes it quite different from imperative languages. This example demonstrates some basic value types and operations, but keep in mind that Idris has many more advanced features, particularly in its type system.