Idris

Idris is a purely-functional programming language with dependent types, quantity annotations, optional lazy evaluation, and features such as a totality checker. Idris is designed to be a general-purpose programming language similar to Haskell, but may also be used as a proof assistant. Wikipedia

Created Year: 2007
Implemented in: Haskell
File extensions: idr, lidr

Wikidata: Q15408477

Influenced by: Agda • Clean • Epigram • Haskell • Rocq prover

Programming paradigms: functional programming • total functional programming • purely functional programming

Language types: purely functional programming language • dependently typed programming language

module Main

main : IO ()
main = putStrLn "Hello World"