Appendix C. REPL commands

The Idris read-eval-print loop (REPL) provides several commands for evaluating and inspecting expressions and types, compiling programs, and searching documentation, among other things. I introduce several of these throughout the book; the following table lists the most commonly used commands, but there are several others available. For more details, type :? at the REPL.

Table 1. Idris REPL commands

Command	Arguments	Description
<expression>	None	Displays the result of evaluating the expression. The variable it contains the result of the most recent evaluation.
:t	<expression>	Displays the type of the expression.
:total	<name>	Displays whether the function with the given name is total.
:doc	<name>	Displays documentation for name.
:let	<definition>	Adds a new definition.
:exec	<expression>	Compiles and executes the expression. If none is given, compiles and executes main.
:c	<output file>	Compiles to an executable with the entry point main.
:r	None	Reloads the current module.
:l	<filename>	Loads a new file.
:module	<module name>	Imports an extra module for use at the REPL.
:printdef	<name>	Displays the definition of name.
:apropos	<word>	Searches function names, types, and documentation for the given word.
:search	<type>	Searches for functions with the given type.
:browse	<namespace>	Displays the names and types defined in the given namespace.
:q	None	Exits the REPL.