idris(1) - f30

1man(1)                          Idris man page                          man(1)
2
3
4

NAME

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

SYNOPSIS

10       idris [ options] [FILES]
11

DESCRIPTION

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
19       + Full dependent types with dependent pattern matching
20
21       + Simple case expressions, where-clauses, with-rule
22
23       + Pattern matching let- and lambda-bindings
24
25       + Overloading via Interfaces (Type class-like), Monad comprehensions
26
27       + do-notation, idiom brackets
28
29       + Syntactic conveniences for lists, tuples, dependent pairs
30
31       + Totality checking
32
33       + Coinductive types
34
35       + Indentation significant syntax, Extensible syntax
36
37       + Tactic based theorem proving (influenced by Coq)
38
39       + Cumulative universes
40
41       + Simple Foreign Function Interface
42
43       + Hugs style interactive environment
44
45       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
50

OPTIONS

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         --consolewidth WIDTH     Select console width: auto, infinite, nat
119         --highlight              Emit source code highlighting
120         --no-tactic-deprecation-warnings
121                                  Disable  deprecation  warnings  for  the old
122       tactic
123                                  sublanguage
124         -v,--version             Print version information
125         -h,--help                Show this help text
126
127

AUTHOR

142       The Idris Community
143
144
145
1461.3.1                           23 October 2018                         man(1)

NAME

SYNOPSIS

DESCRIPTION

OPTIONS

SEE ALSO

AUTHOR