git.iko.soy/Idris-dev
on fdfd99e help sign in
Idris-dev/man/idris.1
94 lines 3.7 kB history raw
1.\" Manpage for Idris.
2.\" Contact <> to correct errors or typos.
3.TH man 1 "06 August 2014" "0.9.14.1" "Idris man page"
4.SH NAME
5idris -\ a general purpose pure functional programming language with dependent types.
6.SH SYNOPSIS
7idris [ options] [FILES]
8.SH DESCRIPTION
9Idris is a general purpose pure functional programming language with
10dependent types. Dependent types allow types to be predicated on
11values, meaning that some aspects of a program’s behaviour can be
12specified precisely in the type. It is compiled, with eager
13evaluation. Its features are influenced by Haskell and ML.
15+ Full dependent types with dependent pattern matching
17+ where clauses, with rule, simple case expressions
19+ pattern matching let and lambda bindings
21+ Type classes, monad comprehensions
23+ do notation, idiom brackets
25+ syntactic conveniences for lists, tuples, dependent pairs
27+ Totality checking
29+ Coinductive types
31+ Indentation significant syntax, extensible syntax
33+ Tactic based theorem proving (influenced by Coq)
35+ Cumulative universes
37+ Simple foreign function interface (to C)
39+ Hugs style interactive environment
41It is important to note that Idris is first and foremost a research tool
42and project. Thus the tooling provided and resulting programs created
43should not necessarily be seen as production ready nor for industrial use.
45.SH OPTIONS
46 --nobanner Suppress the banner
47 -q,--quiet Quiet verbosity
48 --log LEVEL Debugging log level
49 -o,--output FILE Specify output file
50 --total Require functions to be total by default
51 --warnpartial Warn about undeclared partial functions
52 --warnreach Warn about reachable but inaccessible arguments
53 --link Display link flags
54 --libdir Display library directory
55 --include Display the includes flags
56 -V,--verbose Loud verbosity
57 --ibcsubdir FILE Write IBC files into sub directory
58 -i,--idrispath ARG Add directory to the list of import paths
59 --build IPKG Build package
60 --install IPKG Install package
61 --clean IPKG Clean package
62 --mkdoc IPKG Generate IdrisDoc for package
63 --checkpkg IPKG Check package only
64 --testpkg IPKG Run tests for package
65 -S,--codegenonly Do no further compilation of code generator output
66 -c,--compileonly Compile to object files rather than an executable
67 --mvn Create a maven project (for Java codegen)
68 --codegen TARGET Select code generator: C, Java, bytecode
69 -e,--eval EXPR Evaluate an expression without loading the REPL
70 --execute Execute as idris
71 --exec EXPR Execute as idris
72 -X,--extension EXT Turn on language extension (TypeProviders or
73 ErrorReflection)
74 --target TRIPLE Select target triple (for llvm codegen)
75 --cpu CPU Select target CPU e.g. corei7 or cortex-m3 (for LLVM
76 codegen)
77 --color,--colour Force coloured output
78 --nocolor,--nocolour Disable coloured output
79 -v,--version Print version information
80 -h,--help Show this help text
81.SH SEE ALSO
83+ The IDRIS web site (http://idris-lang.org/
85+ The IRC channel #idris, on chat.freenode.net
87+ The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further user provided information, in particular:
89 – https://github.com/idris-lang/Idris-dev/wiki/Manual
91 – https://github.com/idris-lang/Idris-dev/wiki/Language-Features
93.SH AUTHOR
94The Idris Community