-Though ForSyDe offers higher-order functions and polymorphism, ForSyDe's
-choice elements are limited to \hs{if} and \hs{case} expressions. ForSyDe's
-explicit conversions, where functions have to be wrapped in processes and
-processes have to be wrapped in systems, combined with the explicit
-instantiations of components, also makes ForSyDe far more verbose than \CLaSH.
-
-Lava~\cite{Lava,kansaslava} is a hardware description language embedded in
-Haskell which focuses on the structural representation of hardware. Like
-\CLaSH, Lava has support for polymorphic types and higher-order functions.
-Besides support for simulation and circuit synthesis, Lava descriptions can be
-interfaced with formal method tools for formal verification. As discussed in
-the introduction, taking the embedded language approach does not allow for
-Haskell's choice elements to be captured within the circuit descriptions. In
-this respect \CLaSH\ differs from Lava, in that all of Haskell's choice
-elements, such as \hs{case}-expressions and pattern matching, are synthesized
-to choice elements in the eventual circuit. Consequently, descriptions
-containing rich control structures can be specified in a more user-friendly
-way in \CLaSH\ than possible within Lava, and hence are less error-prone.
+Although ForSyDe offers higher-order functions and polymorphism, ForSyDe's
+choice elements are limited to \hs{if-then-else} and \hs{case} expressions.
+ForSyDe's explicit conversions, where functions have to be wrapped in
+processes and processes have to be wrapped in systems, combined with the
+explicit instantiations of components, also makes ForSyDe far more verbose
+than \CLaSH.
+
+Lava~\cite{Lava,kansaslava} is a \acro{HDL} embedded in Haskell which focuses
+on the structural representation of hardware. Like \CLaSH, Lava has support
+for polymorphic types and higher-order functions. Besides support for
+simulation and circuit synthesis, Lava descriptions can be interfaced with
+formal method tools for formal verification. As discussed in the introduction,
+taking the embedded language approach does not allow for Haskell's choice
+elements to be captured within the circuit descriptions. In this respect
+\CLaSH\ differs from Lava, in that all of Haskell's choice elements, such as
+\hs{case}-expressions and pattern matching, are synthesized to choice elements
+in the eventual circuit. Consequently, descriptions containing rich control
+structures can be specified in a more user-friendly way in \CLaSH\ than
+possible within Lava, and hence are less error-prone.