Minor fixes in Float

Chapters/Float.lhs

@@ -27,7 +27,7 @@ We also added:
 \begin{verbatim}
 --abstract-plet       abstract pattern lets in generated code
 \end{verbatim}
-This splits generated function definitions into two functions,
+which splits generated function definitions into two functions,
 the first containing only the top-level pattern bindings and a call to the second, and the second contining only the original body inside those pattern bindings, dependent on the additional variables bound in those patterns.
 
 \section{Logical Representation}
@@ -54,7 +54,15 @@ in f t1 t2
 \label{fig:float_example}
 \end{figure}
 
-Pattern let floating combines the benefits of pattern lets, described in section~\ref{cha:logical_plet}, with the benefits of floating described in Section~\ref{sec:let_floating}. We take inspiration from \citet{jones1996}'s ``Full laziness'' transformation in GHC and apply it to the code generated by the Agda compiler backend. In our pattern let floating optimisation, we float the pattern let as far upwards in an expression tree if and until they can be joined with another floated pattern let on the same variable.  By doing so, we avoid re-computing the same expression when it is used in multiple subexpressions.
+Pattern let floating combines the benefits of pattern lets, described in
+Section~\ref{cha:logical_plet}, with the benefits of floating described in
+Section~\ref{sec:let_floating}. We take inspiration from \citet{jones1996}'s
+``Full laziness'' transformation in GHC and apply it to the code generated by
+the Agda compiler backend. In our pattern let floating optimisation, we float
+the pattern lets as far upwards in an expression tree if and until they can be
+joined with another floated pattern let on the same expression.  By doing so, we
+avoid re-computing the same expression when it is used in multiple
+subexpressions.
 
 \section{Implementation}
 \label{sec:float_implement}