@@ -228,8 +228,24 @@ This is made possible through the following directives:
228228\texttt{-lx} option to \texttt{gcc}.
229229\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.
230230\item \texttt{\%link "x.o"} --- link with the object file \texttt{x.o}.
231+\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.
231232\end{itemize}
232233
234+\subsubsection*{Testing foreign function calls}
235+Normally, the Idris interpreter (used for typechecking and at the REPL) will
236+not perform IO actions. Additionally, as it neither generates C code nor
237+compiles to machine code, the \texttt{\%lib}, \texttt{\%include} and
238+\texttt{\%link} directives have no effect. IO actions and FFI calls can be
239+tested using the special REPL command \texttt{:x EXPR}, and C libraries can be
240+dynamically loaded in the interpreter by using the \texttt{:dynamic} command
241+or the \texttt{\%dynamic} directive. For example:
242+
243+\begin{SaveVerbatim}{xdynamic}
244+Idris> :dynamic libm.so
245+Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
246+0.9995736030415051 : Float
247+\end{SaveVerbatim}
248+\useverb{xdynamic}
233249\subsection{Cumulativity}
234250
235251Since values can appear in types and \emph{vice versa}, it is natural that types themselves