@@ -66,6 +66,7 @@ Note that the \texttt{\$} indicates the shell prompt! Some useful options to the
6666\item \texttt{-o prog} to compile to an executable called \texttt{prog}.
6767\item \texttt{--check} type check the file and its dependencies without starting the
6868interactive environment.
69+\item \texttt{--help} display usage summary and command line options
6970\end{itemize}
7071
7172\subsection{The interactive environment}
@@ -105,15 +106,24 @@ Idris version 0.9.5
105106
106107 <expr> Evaluate an expression
107108 :t <expr> Check the type of an expression
109+ :miss :missing <name> Show missing clauses
110+ :i :info <name> Display information about a type class
108111 :total <name> Check the totality of a name
109112 :r :reload Reload current file
113+ :l :load <filename> Load a new file
114+ :m :module <module> Import an extra module
110115 :e :edit Edit current file using $EDITOR or $VISUAL
111116 :m :metavars Show remaining proof obligations (metavariables)
112117 :p :prove <name> Prove a metavariable
113− :a :addproof Add last proof to source file
118+ :a :addproof <name> Add proof to source file
119+ :rmproof <name> Remove proof from proof stack
120+ :showproof <name> Show proof
121+ :proofs Show available proofs
114122 :c :compile <filename> Compile to an executable <filename>
115123 :exec :execute Compile to an executable and run
116124 :? :h :help Display this help text
125+ :set <option> Set an option (errorcontext, showimplicits)
126+ :unset <option> Unset an option
117127 :q :quit Exit the Idris system
118128\end{SaveVerbatim}
119129\codefigs{cmds}{Interactive environment commands}
@@ -142,7 +152,7 @@ Hello world
142152\codefig{run1}{Sample interactive run}
143153
144154\noindent
145−Type checking a file, if successful, creates a bytecode version of the file (in this
146−case \texttt{hello.ibc}) to speed up loading in future. The bytecode is regenerated if
147−the source file changes.
155+Type checking a file, if successful, creates a bytecode version of the file (in
156+this case \texttt{hello.ibc}) to speed up loading in future. The bytecode is
157+regenerated if the source file changes.
148158