@@ -0,0 +1,94 @@
2+.\" Contact <> to correct errors or typos.
3+.TH man 1 "06 August 2014" "0.9.14.1" "Idris man page"
5+idris -\ a general purpose pure functional programming language with dependent types.
7+idris [ options] [FILES]
9+Idris is a general purpose pure functional programming language with
10+dependent types. Dependent types allow types to be predicated on
11+values, meaning that some aspects of a program’s behaviour can be
12+specified precisely in the type. It is compiled, with eager
13+evaluation. 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
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
41+It is important to note that Idris is first and foremost a research tool
42+and project. Thus the tooling provided and resulting programs created
43+should not necessarily be seen as production ready nor for industrial use.
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 langage extension (TypeProviders or
74+ --target TRIPLE Select target triple (for llvm codegen)
75+ --cpu CPU Select target CPU e.g. corei7 or cortex-m3 (for LLVM
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
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