---
name: "idris"
section: "1"
platform: "linux"
package: "idris"
version: "1.3.4-606"
release: "Arch Linux 2026-11-01"
platforms: ["linux"]
url: "https://new.carta.tech/idris"
---

# idris(1)

a general purpose pure functional programming language with dependent types.

## NAME

idris - a general purpose pure functional programming language with dependent types.

## SYNOPSIS

idris \[ options\] \[FILES\]

## DESCRIPTION

Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation. Its features are influenced by Haskell and ML.

\+ Full dependent types with dependent pattern matching

\+ Simple case expressions, where-clauses, with-rule

\+ Pattern matching let- and lambda-bindings

\+ Overloading via Interfaces (Type class-like), Monad comprehensions

\+ do-notation, idiom brackets

\+ Syntactic conveniences for lists, tuples, dependent pairs

\+ Totality checking

\+ Coinductive types

\+ Indentation significant syntax, Extensible syntax

\+ Tactic based theorem proving (influenced by Coq)

\+ Cumulative universes

\+ Simple Foreign Function Interface

\+ Hugs style interactive environment

It is important to note that Idris is first and foremost a research tool and project. Thus the tooling provided and resulting programs created should not necessarily be seen as production ready nor for industrial use.

## OPTIONS

  \--nobanner               Suppress the banner\
   \-q,--quiet               Quiet verbosity\
   \--ide-mode               Run the Idris REPL with machine-readable syntax\
   \--ide-mode-socket        Choose a socket for IDE mode to listen on\
   \--ideslave               Deprecated version of --ide-mode\
   \--ideslave-socket        Deprecated version of --ide-mode-socket\
   \--log LEVEL              Debugging log level\
   \--logging-categories CATS\
                            Colon separated logging categories. Use --listlogcats\
                            to see list.\
   \--nobasepkgs             Do not use the given base package\
   \--noprelude              Do not use the given prelude\
   \--nobuiltins             Do not use the builtin functions\
   \--check                  Typecheck only, don't start the REPL\
   \-o,--output FILE         Specify output file\
   \--interface              Generate interface files from ExportLists\
   \--typeintype             Turn off Universe checking\
   \--total                  Require functions to be total by default\
   \--warnpartial            Warn about undeclared partial functions\
   \--warnreach              Warn about reachable but inaccessible arguments\
   \--listlogcats            Display logging categories\
   \--link                   Display link flags\
   \--listlibs               Display installed libraries\
   \--libdir                 Display library directory\
   \--include                Display the includes flags\
   \--V2                     Loudest verbosity\
   \--V1                     Louder verbosity\
   \-V, --V0, --verbose      Loud verbosity\
   \--ibcsubdir FILE         Write IBC files into sub directory\
   \-i,--idrispath ARG       Add directory to the list of import paths\
   \--sourcepath ARG         Add directory to the list of source search paths\
   \-p,--package ARG         Add package as a dependency\
   \--port PORT              REPL TCP port\
   \--build IPKG             Build package\
   \--install IPKG           Install package\
   \--repl IPKG              Launch REPL, only for executables\
   \--clean IPKG             Clean package\
   \--mkdoc IPKG             Generate IdrisDoc for package\
   \--checkpkg IPKG          Check package only\
   \--testpkg IPKG           Run tests for package\
   \-S,--codegenonly         Do no further compilation of code generator output\
   \-c,--compileonly         Compile to object files rather than an executable\
   \--codegen TARGET         Select code generator: C, Javascript, Node and\
                            bytecode are bundled with Idris\
   \--cg-opt ARG             Arguments to pass to code generator\
   \-e,--eval EXPR           Evaluate an expression without loading the REPL\
   \--execute                Execute as idris\
   \--exec EXPR              Execute as idris\
   \-X,--extension EXT       Turn on language extension (TypeProviders or\
                            ErrorReflection)\
   \--partial-eval           Switch on partial evaluation\
   \--target TRIPLE          If supported the codegen will target the named triple.\
   \--cpu CPU                If supported the codegen will target the named CPU\
                            e.g. corei7 or cortex-m3.\
   \--color,--colour         Force coloured output\
   \--nocolor,--nocolour     Disable coloured output\
   \--optimise-nat-like-types,--optimize-nat-like-types\
                            Compile Nat-like types to big ints\
   \--no-optimise-nat-like-types,--no-optimize-nat-like-types\
                            Do not compile Nat-like types to big ints\
   \--consolewidth WIDTH     Select console width: auto, infinite, nat\
   \--highlight              Emit source code highlighting\
   \--no-tactic-deprecation-warnings\
                            Disable deprecation warnings for the old tactic\
                            sublanguage\
   \-v,--version             Print version information\
   \-h,--help                Show this help text

## SEE ALSO

\+ The IDRIS web site (https://idris-lang.org/

\+  The IRC channel #idris, on chat.freenode.net

\+ The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further user provided information, in particular:

  – https://github.com/idris-lang/Idris-dev/wiki/Manual

  – https://github.com/idris-lang/Idris-dev/wiki/Language-Features

## AUTHOR

The Idris Community