1man(1) Idris man page man(1)
2
6 idris - a general purpose pure functional programming language with
7 dependent types.
8
10 idris [ options] [FILES]
11
13 Idris is a general purpose pure functional programming language with
14 dependent types. Dependent types allow types to be predicated on val‐
15 ues, meaning that some aspects of a program’s behaviour can be speci‐
16 fied precisely in the type. It is compiled, with eager evaluation. Its
17 features are influenced by Haskell and ML.
18 + Full dependent types with dependent pattern matching
20 + Simple case expressions, where-clauses, with-rule
22 + Pattern matching let- and lambda-bindings
24 + Overloading via Interfaces (Type class-like), Monad comprehensions
26 + do-notation, idiom brackets
28 + Syntactic conveniences for lists, tuples, dependent pairs
30 + Totality checking
32 + Coinductive types
34 + Indentation significant syntax, Extensible syntax
36 + Tactic based theorem proving (influenced by Coq)
38 + Cumulative universes
40 + Simple Foreign Function Interface
42 + Hugs style interactive environment
44 It is important to note that Idris is first and foremost a research
46 tool and project. Thus the tooling provided and resulting programs cre‐
47 ated should not necessarily be seen as production ready nor for indus‐
48 trial use.
49
52 --nobanner Suppress the banner
53 -q,--quiet Quiet verbosity
54 --ide-mode Run the Idris REPL with machine-readable
55 syntax
56 --ide-mode-socket Choose a socket for IDE mode to listen on
57 --ideslave Deprecated version of --ide-mode
58 --ideslave-socket Deprecated version of --ide-mode-socket
59 --log LEVEL Debugging log level
60 --logging-categories CATS
61 Colon separated logging categories. Use
62 --listlogcats
63 to see list.
64 --nobasepkgs Do not use the given base package
65 --noprelude Do not use the given prelude
66 --nobuiltins Do not use the builtin functions
67 --check Typecheck only, don't start the REPL
68 -o,--output FILE Specify output file
69 --interface Generate interface files from ExportLists
70 --typeintype Turn off Universe checking
71 --total Require functions to be total by default
72 --warnpartial Warn about undeclared partial functions
73 --warnreach Warn about reachable but inaccessible argu‐
74 ments
75 --listlogcats Display logging categories
76 --link Display link flags
77 --listlibs Display installed libraries
78 --libdir Display library directory
79 --include Display the includes flags
80 --V2 Loudest verbosity
81 --V1 Louder verbosity
82 -V, --V0, --verbose Loud verbosity
83 --ibcsubdir FILE Write IBC files into sub directory
84 -i,--idrispath ARG Add directory to the list of import paths
85 --sourcepath ARG Add directory to the list of source search
86 paths
87 -p,--package ARG Add package as a dependency
88 --port PORT REPL TCP port
89 --build IPKG Build package
90 --install IPKG Install package
91 --repl IPKG Launch REPL, only for executables
92 --clean IPKG Clean package
93 --mkdoc IPKG Generate IdrisDoc for package
94 --checkpkg IPKG Check package only
95 --testpkg IPKG Run tests for package
96 -S,--codegenonly Do no further compilation of code generator
97 output
98 -c,--compileonly Compile to object files rather than an exe‐
99 cutable
100 --codegen TARGET Select code generator: C, Javascript, Node
101 and
102 bytecode are bundled with Idris
103 --cg-opt ARG Arguments to pass to code generator
104 -e,--eval EXPR Evaluate an expression without loading the
105 REPL
106 --execute Execute as idris
107 --exec EXPR Execute as idris
108 -X,--extension EXT Turn on language extension (TypeProviders or
109 ErrorReflection)
110 --partial-eval Switch on partial evaluation
111 --target TRIPLE If supported the codegen will target the
112 named triple.
113 --cpu CPU If supported the codegen will target the
114 named CPU
115 e.g. corei7 or cortex-m3.
116 --color,--colour Force coloured output
117 --nocolor,--nocolour Disable coloured output
118 --optimise-nat-like-types,--optimize-nat-like-types
119 Compile Nat-like types to big ints
120 --no-optimise-nat-like-types,--no-optimize-nat-like-types
121 Do not compile Nat-like types to big ints
122 --consolewidth WIDTH Select console width: auto, infinite, nat
123 --highlight Emit source code highlighting
124 --no-tactic-deprecation-warnings
125 Disable deprecation warnings for the old
126 tactic
127 sublanguage
128 -v,--version Print version information
129 -h,--help Show this help text
130
133 + The IDRIS web site (https://idris-lang.org/
134 + The IRC channel #idris, on chat.freenode.net
136 + The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further
138 user provided information, in particular:
139 – https://github.com/idris-lang/Idris-dev/wiki/Manual
141 – https://github.com/idris-lang/Idris-dev/wiki/Language-Features
143
146 The Idris Community
1471.3.3 23 May 2020 man(1)