7Idris comes with a ``REPL``.
12Being a fully dependently typed language, Idris has two phases where it
13evaluates things, compile-time and run-time. At compile-time it will only
14evaluate things which it knows to be total (i.e. terminating and covering all
15possible inputs) in order to keep type checking decidable. The compile-time
16evaluator is part of the Idris kernel, and is implemented in Haskell using a
17HOAS (higher order abstract syntax) style representation of values. Since
18everything is known to have a normal form here, the evaluation strategy doesn't
19actually matter because either way it will get the same answer, and in practice
20it will do whatever the Haskell run-time system chooses to do.
22The REPL, for convenience, uses the compile-time notion of evaluation. As well
23as being easier to implement (because we have the evaluator available) this can
24be very useful to show how terms evaluate in the type checker. So you can see
25the difference between:
29 Idris> \n, m => (S n) + m
30 \n => \m => S (plus n m) : Nat -> Nat -> Nat
32 Idris> \n, m => n + (S m)
33 \n => \m => plus n (S m) : Nat -> Nat -> Nat
38Idris supports initialisation scripts.
43When the Idris REPL starts up, it will attempt to open the file
44repl/init in Idris's application data directory. The application data
45directory is the result of the Haskell function call
46``getAppUserDataDirectory "idris"``, which on most Unix-like systems
47will return $HOME/.idris and on various versions of Windows will return
48paths such as ``C:/Documents And Settings/user/Application Data/appName``.
50The file repl/init is a newline-separate list of REPL commands. Not all
51commands are supported in initialisation scripts — only the subset that
52will not interfere with the normal operation of the REPL. In particular,
53setting colours, display options such as showing implicits, and log
56Example initialisation script
57~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
60 :colour prompt white italic bold
61 :colour implicit magenta italic
68The current set of supported commands are:
70+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
71|Command | Arguments | Purpose |
72+================+==============================+==========================================================================================================+
73|<expr> | | Evaluate an expression |
74+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
75|:t :type | <expr> | Check the type of an expression |
76+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
77|:core | <expr> | View the core language representation of a term |
78+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
79|:miss :missing | <name> | Show missing clauses |
80+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
81|:doc | <name> | Show internal documentation |
82+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
83|:mkdoc | <namespace> | Generate IdrisDoc for namespace(s) and dependencies |
84+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
85|:apropos | [<package list>] <name> | Search names, types, and documentation |
86+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
87|:s :search | [<package list>] <expr> | Search for values by type |
88+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
89|:wc :whocalls | <name> | List the callers of some name |
90+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
91|:cw :callswho | <name> | List the callees of some name |
92+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
93|:browse | <namespace> | List the contents of some namespace |
94+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
95|:total | <name> | Check the totality of a name |
96+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
97|:r :reload | | Reload current file |
98+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
99|:l :load | <filename> | Load a new file |
100+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
101|:cd | <filename> | Change working directory |
102+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
103|:module | <module> | Import an extra module |
104+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
105|:e :edit | | Edit current file using $EDITOR or $VISUAL |
106+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
107|:m :metavars | | Show remaining proof obligations (holes) |
108+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
109|:p :prove | <hole> | Prove a hole |
110+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
111|:a :addproof | <name> | Add proof to source file |
112+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
113|:rmproof | <name> | Remove proof from proof stack |
114+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
115|:showproof | <name> | Show proof |
116+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
117|:proofs | | Show available proofs |
118+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
119|:x | <expr> | Execute IO actions resulting from an expression using the interpreter |
120+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
121|:c :compile | <filename> | Compile to an executable [codegen] <filename> |
122+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
123|:exec :execute | [<expr>] | Compile to an executable and run |
124+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
125|:dynamic | <filename> | Dynamically load a C library (similar to %dynamic) |
126+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
127|:dynamic | | List dynamically loaded C libraries |
128+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
129|:? :h :help | | Display this help text |
130+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
131|:set | <option> | Set an option (errorcontext, showimplicits, originalerrors, autosolve, nobanner, warnreach, evaltypes, |
133+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
134|:unset | <option> | Unset an option |
135+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
136|:color :colour | <option> | Turn REPL colours on or off; set a specific colour |
137+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
138|:consolewidth | auto|infinite|<number> | Set the width of the console |
139+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
140|:printerdepth | <number-or-blank> | Set the maximum pretty-printing depth, or infinite if nothing specified |
141+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
142|:q :quit | | Exit the Idris system |
143+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
144|:w :warranty | | Displays warranty information |
145+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
146|:let | (<top-level-declaration>)... | Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration |
147+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
148|:unlet :undefine|(<name>)... | Remove the listed repl definitions, or all repl definitions if no names given |
149+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
150|:printdef | <name> | Show the definition of a function |
151+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
152|:pp :pprint | <option> <number> <name> | Pretty prints an Idris function in either LaTeX or HTML and for a specified width. |
153+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
163The command ``:help`` (or ``:h`` or ``:?``) prints a short summary of
164the available commands.
169If you would like to leave Idris, simply use ``:q`` or ``:quit``.
171Evaluating expressions
172~~~~~~~~~~~~~~~~~~~~~~
174To evaluate an expression, simply type it. If Idris is unable to infer
175the type, it can be helpful to use the operator ``the`` to manually
176provide one, as Idris's syntax does not allow for direct type
177annotations. Examples of ``the`` include:
185 Idris> the (List Nat) [1,2]
187 Idris> the (Vect _ Nat) [1,2]
190This may not work in cases where the expression still involves ambiguous
191names. The name can be disambiguated by using the ``with`` keyword:
196 When elaborating an application of function Prelude.Foldable.sum:
197 Can't disambiguate name: Prelude.List.::,
200 Idris> with List sum [1,2,3]
206To add a let binding to the REPL, use ``:let``. It's likely you'll also
207need to provide a type annotation. ``:let`` also works for other
208declarations as well, such as ``data``.
212 Idris> :let x : String; x = "hello"
215 Idris> :let data Foo : Type where Bar : Foo
219Getting type information
220~~~~~~~~~~~~~~~~~~~~~~~~
222To ask Idris for the type of some expression, use the ``:t`` command.
223Additionally, if used with an overloaded name, Idris will provide all
224overloadings and their types. To ask for the type of an infix operator,
225surround it in parentheses.
232 Prelude.Nat.plus : Nat -> Nat -> Nat
234 Builtins.++ : String -> String -> String
235 Prelude.List.++ : (List a) -> (List a) -> List a
236 Prelude.Vect.++ : (Vect m a) -> (Vect n a) -> Vect (m + n) a
238 plus (Builtins.fromInteger 4) : Nat -> Nat
240You can also ask for basic information about typeclasses with ``:doc``:
251 (>>=) : Monad m => m a -> (a -> m b) -> m b
263Other documentation is also available from ``:doc``:
268 Prelude.Classes.+ : (a : Type) -> (Num a) -> a -> a -> a
273 Class constraint Prelude.Classes.Num a
280 Data type Prelude.Vect.Vect : Nat -> Type -> Type
288 Prelude.Vect.Nil : (a : Type) -> Vect 0 a
291 Prelude.Vect.:: : (a : Type) -> (n : Nat) -> a -> (Vect n a) -> Vect (S n) a
302 Type class Prelude.Monad.Monad
305 Prelude.Monad.>>= : (m : Type -> Type) -> (a : Type) -> (b : Type) -> (Monad m) -> (m a) -> (a -> m b) -> m b
310 Class constraint Prelude.Monad.Monad m
317The command ``:apropos`` searches names, types, and documentation for
318some string, and prints the results. For example:
323 eqPtr : Ptr -> Ptr -> IO Bool
326 eqSucc : (left : Nat) -> (right : Nat) -> (left = right) -> S left = S right
329 lemma_both_neq : ((x = x') -> _|_) -> ((y = y') -> _|_) -> ((x, y) = (x', y')) -> _|_
332 lemma_fst_neq_snd_eq : ((x = x') -> _|_) -> (y = y') -> ((x, y) = (x', y)) -> _|_
335 lemma_snd_neq : (x = x) -> ((y = y') -> _|_) -> ((x, y) = (x, y')) -> _|_
338 lemma_x_eq_xs_neq : (x = y) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_
341 lemma_x_neq_xs_eq : ((x = y) -> _|_) -> (xs = ys) -> (x :: xs = y :: ys) -> _|_
344 lemma_x_neq_xs_neq : ((x = y) -> _|_) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_
347 prim__eqB16 : Bits16 -> Bits16 -> Int
349 prim__eqB16x8 : Bits16x8 -> Bits16x8 -> Bits16x8
351 prim__eqB32 : Bits32 -> Bits32 -> Int
353 prim__eqB32x4 : Bits32x4 -> Bits32x4 -> Bits32x4
355 prim__eqB64 : Bits64 -> Bits64 -> Int
357 prim__eqB64x2 : Bits64x2 -> Bits64x2 -> Bits64x2
359 prim__eqB8 : Bits8 -> Bits8 -> Int
361 prim__eqB8x16 : Bits8x16 -> Bits8x16 -> Bits8x16
363 prim__eqBigInt : Integer -> Integer -> Int
365 prim__eqChar : Char -> Char -> Int
367 prim__eqFloat : Float -> Float -> Int
369 prim__eqInt : Int -> Int -> Int
371 prim__eqString : String -> String -> Int
373 prim__syntactic_eq : (a : Type) -> (b : Type) -> (x : a) -> (y : b) -> Maybe (x = y)
375 sequence : Traversable t => Applicative f => (t (f a)) -> f (t a)
378 sequence_ : Foldable t => Applicative f => (t (f a)) -> f ()
382 The Eq class defines inequality and equality.
384 GTE : Nat -> Nat -> Type
385 Greater than or equal to
387 LTE : Nat -> Nat -> Type
388 Proofs that n is less than or equal to m
390 gte : Nat -> Nat -> Bool
391 Boolean test than one Nat is greater than or equal to another
393 lte : Nat -> Nat -> Bool
394 Boolean test than one Nat is less than or equal to another
397 Convert the number to its ASCII equivalent.
399 replace : (x = y) -> (P x) -> P y
400 Perform substitution in a term according to some equality.
402 sym : (l = r) -> r = l
403 Symmetry of propositional equality
405 trans : (a = b) -> (b = c) -> a = c
406 Transitivity of propositional equality
408``:search`` does a type-based search, in the spirit of Hoogle. See `Type-directed search (:search) <https://github.com/idris-lang/Idris-dev/wiki/Type-directed-search-%28%3Asearch%29>`_ for more details. Here is an example:
412 Idris> :search a -> b -> a
413 = Prelude.Basics.const : a -> b -> a
414 Constant function. Ignores its second argument.
416 = assert_smaller : a -> b -> b
417 Assert to the totality checker than y is always structurally
418 smaller than x (which is typically a pattern argument)
420 > malloc : Int -> a -> a
423 > Prelude.pow : Num a => a -> Nat -> a
426 > Prelude.Classes.(*) : Num a => a -> a -> a
429 > Prelude.Classes.(+) : Num a => a -> a -> a
432``:search`` can also look for dependent types:
436 Idris> :search plus (S n) n = plus n (S n)
437 < Prelude.Nat.plusSuccRightSucc : (left : Nat) ->
439 S (left + right) = left + S right
441Loading and reloading Idris code
442~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
444The command ``:l File.idr`` will load File.idr into the
445currently-running REPL, and ``:r`` will reload the last file that was
451All Idris definitions are checked for totality. The command
452``:total <NAME>`` will display the result of that check. If a definition
453is not total, this may be due to an incomplete pattern match. If that is
454the case, ``:missing`` or ``:miss`` will display the missing cases.
459The command ``:e`` launches your default editor on the current module.
460After control returns to Idris, the file is reloaded.
465The current module can be compiled to an executable using the command
466``:c <FILENAME>`` or ``:compile <FILENAME>``. This command allows to
467specify codegen, so for example JavaScript can be generated using
468``:c javascript <FILENAME>``. The ``:exec`` command will compile the
469program to a temporary file and run the resulting executable.
474Unlike GHCI, the Idris REPL is not inside of an implicit IO monad. This
475means that a special command must be used to execute IO actions.
476``:x tm`` will execute the IO action ``tm`` in an Idris interpreter.
478Dynamically loading C libraries
479~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
481Sometimes, an Idris program will depend on external libraries written in
482C. In order to use these libraries from the Idris interpreter, they must
483first be dynamically loaded. This is achieved through the
484``%dynamic <LIB>`` directive in Idris source files or through the
485``:dynamic <LIB>`` command at the REPL. The current set of dynamically
486loaded libraries can be viewed by executing ``:dynamic`` with no
487arguments. These libraries are available through the Idris FFI in `type
488providers <#type-providers>`__ and ``:exec``.
493Idris terms are available in amazing colour! By default, the Idris REPL
494uses colour to distinguish between data constructors, types or type
495constructors, operators, bound variables, and implicit arguments. This
496feature is available on all POSIX-like systems, and there are plans to
497allow it to work on Windows as well.
499If you do not like the default colours, they can be turned off using the
506and, when boredom strikes, they can be re-enabled using the command
512To modify a colour, use the command
516 :colour <CATEGORY> <OPTIONS>
518where ``<CATEGORY`` is one of ``keyword``, ``boundvar``, ``implicit``,
519``function``, ``type``, ``data``, or ``prompt``, and is a
520space-separated list drawn from the colours and the font options. The
521available colours are ``default``, ``black``, ``yellow``, ``cyan``,
522``red``, ``blue``, ``white``, ``green``, and ``magenta``. If more than
523one colour is specified, the last one takes precedence. The available
524options are ``dull`` and ``vivid``, ``bold`` and ``nobold``, ``italic``
525and ``noitalic``, ``underline`` and ``nounderline``, forming pairs of
526opposites. The colour ``default`` refers to your terminal's default
529The colours used at startup can be changed using REPL initialisation
532Colour can be disabled at startup by the ``--nocolour`` command-line
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list