@@ -66,6 +66,7 @@ Note that the \texttt{\$} indicates the shell prompt! Some useful options to the
66\item \texttt{-o prog} to compile to an executable called \texttt{prog}.
66\item \texttt{-o prog} to compile to an executable called \texttt{prog}.
67\item \texttt{--check} type check the file and its dependencies without starting the
67\item \texttt{--check} type check the file and its dependencies without starting the
68interactive environment.
68interactive environment.
69+\item \texttt{--help} display usage summary and command line options
69\end{itemize}
70\end{itemize}
71\subsection{The interactive environment}
72\subsection{The interactive environment}
@@ -105,15 +106,24 @@ Idris version 0.9.5
106 <expr> Evaluate an expression
107 <expr> Evaluate an expression
107 :t <expr> Check the type of an expression
108 :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
108 :total <name> Check the totality of a name
111 :total <name> Check the totality of a name
109 :r :reload Reload current file
112 :r :reload Reload current file
113+ :l :load <filename> Load a new file
114+ :m :module <module> Import an extra module
110 :e :edit Edit current file using $EDITOR or $VISUAL
115 :e :edit Edit current file using $EDITOR or $VISUAL
111 :m :metavars Show remaining proof obligations (metavariables)
116 :m :metavars Show remaining proof obligations (metavariables)
112 :p :prove <name> Prove a metavariable
117 :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
114 :c :compile <filename> Compile to an executable <filename>
122 :c :compile <filename> Compile to an executable <filename>
115 :exec :execute Compile to an executable and run
123 :exec :execute Compile to an executable and run
116 :? :h :help Display this help text
124 :? :h :help Display this help text
125+ :set <option> Set an option (errorcontext, showimplicits)
126+ :unset <option> Unset an option
117 :q :quit Exit the Idris system
127 :q :quit Exit the Idris system
118\end{SaveVerbatim}
128\end{SaveVerbatim}
119\codefigs{cmds}{Interactive environment commands}
129\codefigs{cmds}{Interactive environment commands}
@@ -142,7 +152,7 @@ Hello world
142\codefig{run1}{Sample interactive run}
152\codefig{run1}{Sample interactive run}
145−Type checking a file, if successful, creates a bytecode version of the file (in this
155+Type checking a file, if successful, creates a bytecode version of the file (in
146−case \texttt{hello.ibc}) to speed up loading in future. The bytecode is regenerated if
156+this case \texttt{hello.ibc}) to speed up loading in future. The bytecode is
147−the source file changes.
157+regenerated if the source file changes.