Changeset 812

Timestamp:

May 16, 2011, 5:43:15 PM (9 years ago)

Author:

mulligan

Message:

small change

File:

• Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) (1 diff)

Deliverables/D4.1/ITP-Paper/itp-2011.tex

@@ -358 +358 @@
 To avoid difficult-to-trace size mismatch bugs, we represented all quantities using bitvectors, i.e. fixed length vectors of booleans.
 In the O'Caml emulator, we `faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
-From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
-However, the module's interface (right column) enforces size invariants in the rest of the code.
+From within the bitvector module (top) bitvectors are just lists of bits and no guarantee is provided on sizes.
+However, the module's interface (bottom) enforces size invariants in the rest of the code.
 
 In Matita, we are able to use the full power of dependent types to always work with vectors of a known size: