-Once the connection with the device is established, \ldots
-\begin{lstClean}
-liftmTask :: (Main (BCInterpret (TaskValue u))) MTDevice -> Task u | iTask u
+Once the connection with the device is established, \gls{MTASK} tasks can be lifted to \gls{MTASK} tasks using the \cleaninline{liftmTask} family of functions (see \cref{lst:liftmtask}).
+Given an \gls{MTASK} task in the \cleaninline{BCInterpret} view and a device obtained from \cleaninline{withDevice}, an \gls{ITASK} task is returned.
+This \gls{ITASK} task tethers the \gls{MTASK} task that is executed on the microcontroller.
+Hence, when for example observing the task value, the actual task value from the microcontroller is observed.
+
+\begin{lstClean}[label={lst:liftmtask},caption={The interface for lifting \gls{MTASK} tasks to \gls{ITASK} tasks.}]
+liftmTask :: (Main (MTask BCInterpret u)) MTDevice -> Task u | iTask u