@@ -72,6 +72,38 @@ head (x :: xs) = x
7272\end{SaveVerbatim}
7373\useverb{defimp}
7474
75+\subsection{Implicit conversions}
76+
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:
81+
82+\begin{SaveVerbatim}{implicit}
83+
84+implicit intString : Int -> String
85+intString = show
86+
87+test : Int -> String
88+test x = "Number " ++ x
89+
90+\end{SaveVerbatim}
91+\useverb{implicit}
92+
93+\noindent
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.
99+
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.
106+
75107\subsection{Literate programming}
76108
77109Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an