@@ -72,6 +72,38 @@ head (x :: xs) = x
72\end{SaveVerbatim}
72\end{SaveVerbatim}
73\useverb{defimp}
73\useverb{defimp}
75+\subsection{Implicit conversions}
77+\Idris{} supports the creation of \emph{implicit conversions}, which allow
78+automatic conversion of values from one type to another when required to make
79+a term type correct. This is intended to increase convenience and reduce
80+verbosity. A contrived but simple example is the following:
82+\begin{SaveVerbatim}{implicit}
84+implicit intString : Int -> String
88+test x = "Number " ++ x
94+In general, we cannot append an \texttt{Int} to a \texttt{String}, but the
95+implicit conversion function \texttt{intString} can convert \texttt{x} to a
96+\texttt{String}, so the definition of \texttt{test} is type correct. An
97+implicit conversion is implemented just like any other function, but given
98+the \texttt{implicit} modifier, and restricted to one explicit argument.
100+Only one implicit conversion will be applied at a time. That is, implicit
101+conversions cannot be chained.
102+Implicit conversions of simple types, as above, are however discouraged! More
103+commonly, an implicit conversion would be used to reduce verbosity in an
104+embedded domain specific language, or to hide details of a proof. Such examples
105+are beyond the scope of this tutorial.
75\subsection{Literate programming}
107\subsection{Literate programming}
77Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an
109Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an