Idris is an actively used programming language created in 2014. Idris is a general-purpose purely functional programming language with dependent types, strict or optional lazy evaluation and features such as a totality checker. Even before its possible usage for interactive theorem-proving, the focus of Idris is on general-purpose programming, like the purely functional Haskell, and with sufficient performance. The type system of Idris is similar to the one used by Agda and theorem-proving in it is similar to Coq, including tactics. Read more on Wikipedia...

5Years Old 4,923Users 2Jobs

Example code from the Hello World Collection:

Hello world in Idris

> main : IO ()
> main = putStrLn "Hello, World!"

Example code from Linguist:

module Prelude.Char

import Builtins

isUpper : Char -> Bool
isUpper x = x >= 'A' && x <= 'Z'

isLower : Char -> Bool
isLower x = x >= 'a' && x <= 'z'

isAlpha : Char -> Bool
isAlpha x = isUpper x || isLower x

isDigit : Char -> Bool
isDigit x = (x >= '0' && x <= '9')

isAlphaNum : Char -> Bool
isAlphaNum x = isDigit x || isAlpha x

isSpace : Char -> Bool
isSpace x = x == ' '  || x == '\t' || x == '\r' ||
            x == '\n' || x == '\f' || x == '\v' ||
            x == '\xa0'

isNL : Char -> Bool
isNL x = x == '\r' || x == '\n'

toUpper : Char -> Char
toUpper x = if (isLower x)
               then (prim__intToChar (prim__charToInt x - 32))
               else x

toLower : Char -> Char
toLower x = if (isUpper x)
               then (prim__intToChar (prim__charToInt x + 32))
               else x

isHexDigit : Char -> Bool
isHexDigit x = elem (toUpper x) hexChars where
  hexChars : List Char
  hexChars = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
              'A', 'B', 'C', 'D', 'E', 'F']

Example code from Wikipedia:

total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil       Nil       = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys

Trending Repos

repo stars description

Last updated December 10th, 2019

Edit Idris