typo: fix contraction of "let us"

Author: dijkstracula

src/Tutorial_02_Logic.lhs

@@ -274,7 +274,7 @@ sophisticated abstractions.]
 Examples: Propositions
 ----------------------
 
-Finally, lets conclude this quick overview with some
+Finally, let's conclude this quick overview with some
 examples of predicates, in order to build up our own
 intuition about logic and validity.
 Each of the below is a predicate from our refinement
@@ -390,7 +390,7 @@ exDeMorgan2 a b = not (a && b) <=> (not a && not b)
 Examples: Arithmetic
 --------------------
 
-Next, lets look at some predicates involving arithmetic.
+Next, let's look at some predicates involving arithmetic.
 The simplest ones don't have any variables, for example:
 
 \begin{code}
@@ -487,8 +487,8 @@ fx1 f x =   (x == f (f (f x)))
         ==> (x == f x)
 \end{code}
 
-To get a taste of why uninterpreted functions will prove useful
-lets write a function to compute the `size` of a list:
+To get a taste of why uninterpreted functions will prove useful,
+let's write a function to compute the `size` of a list:
 
 \begin{code}
 {-@ measure size @-}
@@ -546,5 +546,5 @@ mean by the term *logical predicate*.
    and evaluating the predicates (which would take forever!) but instead
    by using clever symbolic algorithms.
 
-Next, lets see how we can use logical predicates to *specify* and
+Next, let's see how we can use logical predicates to *specify* and
 *verify* properties of real programs.

src/Tutorial_05_Datatypes.lhs

@@ -288,12 +288,12 @@ badList = 2 :< 1 :< 3 :< Emp      -- rejected by LH
 
 \noindent
 It's all very well to *specify* ordered lists.
-Next, lets see how it's equally easy to *establish*
+Next, let's see how it's equally easy to *establish*
 these invariants by implementing several textbook
 sorting routines.
 
 \newthought{Insertion Sort}
-First, lets implement insertion sort, which converts an ordinary
+First, let's implement insertion sort, which converts an ordinary
 list `[a]` into an ordered list `IncList a`.
 
 \begin{code}
@@ -527,11 +527,11 @@ add k' t@(Node k l r)
   | otherwise        = t
 \end{code}
 
-\newthought{Minimum} For our next trick, lets write a function to delete the *minimum*
-element from a `BST`. This function will return a *pair* of outputs --
-the smallest element and the remainder of the tree. We can say that the
+\newthought{Minimum} For our next trick, let's write a function to delete the
+*minimum* element from a `BST`. This function will return a *pair* of outputs
+-- the smallest element and the remainder of the tree. We can say that the
 output element is indeed the smallest, by saying that the remainder's
-elements exceed the element. To this end, lets define a helper type:
+elements exceed the element. To this end, let's define a helper type:
 ^[This helper type approach is rather verbose.
 We should be able to just use plain old pairs
 and specify the above requirement as a *dependency*

src/Tutorial_06_Measure_Bool.lhs

@@ -5,7 +5,7 @@ Boolean Measures {#boolmeasures}
 
 In the last two chapters, we saw how refinements could be used to
 reason about the properties of basic `Int` values like vector
-indices, or the elements of a list. Next, lets see how we can
+indices, or the elements of a list. Next, let's see how we can
 describe properties of aggregate structures like lists and trees,
 and use these properties to improve the APIs for operating over
 such structures.
@@ -74,7 +74,7 @@ avg3 x y z = divide (x + y + z) 3
 \end{code}
 
 \noindent However, it can be more of a challenge when the divisor
-is obtained *dynamically*. For example, lets write a function to
+is obtained *dynamically*. For example, let's write a function to
 find the number of elements in a list
 
 \begin{code}
@@ -117,7 +117,7 @@ Lifting Functions to Measures {#usingmeasures}
 
 \newthought{How} shall we tell LiquidHaskell that a list is *non-empty*?
 Recall the notion of `measure` previously [introduced](#vectorbounds)
-to describe the size of a `Data.Vector`. In that spirit, lets write
+to describe the size of a `Data.Vector`. In that spirit, let's write
 a function that computes whether a list is not empty:
 
 \begin{code}
@@ -387,7 +387,7 @@ In this chapter we saw how LiquidHaskell lets you
    often clutter implementations and specifications.
 
 \noindent
-Of course, we can do a lot more with measures, so lets press on!
+Of course, we can do a lot more with measures, so let's press on!
 
 
 

src/Tutorial_07_Measure_Int.lhs

@@ -68,7 +68,7 @@ we will use this API to implement K-means clustering.]
 Wholemeal Programming
 ---------------------
 
-Indexitis begone! As an example of wholemeal programming, lets
+Indexitis begone! As an example of wholemeal programming, let's
 write a small library that represents vectors as lists and
 matrices as nested vectors:
 
@@ -211,7 +211,7 @@ We are almost ready to begin creating a dimension aware API
 for lists; one last thing that is useful is a couple of aliases
 for describing lists of a given dimension.
 
-\newthought{To make signatures symmetric} lets define an alias for
+\newthought{To make signatures symmetric} let's define an alias for
 plain old (unrefined) lists:
 
 \begin{code}
@@ -345,7 +345,7 @@ test3     = zipOrNull ["cat", "dog"] []
 Lists: Size Reducing API {#listreducing}
 ------------------------
 
-Next, lets look at some functions that truncate lists, in one way or another.
+Next, let's look at some functions that truncate lists, in one way or another.
 
 \newthought{Take} lets us grab the first `k` elements from a list:
 
@@ -685,7 +685,7 @@ mat23     = matFromList [ [1, 2]
 How will you figure out the number of columns? A measure
 may be useful.
 
-\newthought{Matrix Multiplication} Finally, lets implement matrix
+\newthought{Matrix Multiplication} Finally, let's implement matrix
 multiplication. You'd think we did it already, but in fact the
 implementation at the top of this chapter is all wrong (run it and
 see!) We cannot just multiply any two matrices: the number of

src/Tutorial_08_Measure_Set.lhs

@@ -70,15 +70,15 @@ Examples of this abound: for example, we'd like to know that:
 \newthought{SMT Solvers} support very expressive logics.
 In addition to linear arithmetic and uninterpreted functions,
 they can [efficiently decide][smt-set] formulas over sets.
-Next, lets see how LiquidHaskell lets us exploit this fact
+Next, let's see how LiquidHaskell lets us exploit this fact
 to develop types and interfaces that guarantee invariants
 over the set of elements of a structures.
 
 Talking about Sets
 ------------------
 
 First, we need a way to talk about sets in the refinement logic. We could
-roll our own special Haskell type but for now, lets just use the `Set a`
+roll our own special Haskell type but for now, let's just use the `Set a`
 type from the prelude's `Data.Set`.^[See [this](https://ucsd-progsys.github.io/liquidhaskell-blog/2013/03/26/talking-about-sets.lhs/)
 for a brief description of how to work directly with the set operators natively
 supported by LiquidHaskell.]
@@ -114,7 +114,7 @@ to learn how modern SMT solvers prove equalities like the above.]
 Proving QuickCheck Style Properties {#quickcheck}
 -----------------------------------
 
-To get the hang of whats going on, lets do a few warm up exercises,
+To get the hang of whats going on, let's do a few warm up exercises,
 using LiquidHaskell to prove various simple theorems about sets
 and operations over them.
 
@@ -206,7 +206,7 @@ prop_union_assoc x y z
 
 \newthought{The Distributivity Laws} for Boolean Algebra can
 be verified by writing properties over the relevant operators.
-For example, we lets check that `intersection` distributes over `union`:
+For example, let's check that `intersection` distributes over `union`:
 
 \begin{code}
 {-@ prop_intersection_dist :: _ -> _ -> _ -> True @-}
@@ -398,10 +398,10 @@ test2      = elem 2 [1, 3]
 Permutations
 ------------
 
-Next, lets use the refined list API to prove that
+Next, let's use the refined list API to prove that
 various sorting routines return *permutations*
 of their inputs, that is, return output lists whose
-elements are the *same as* those of the input lists.^[Since we are focusing on the elements, lets not
+elements are the *same as* those of the input lists.^[Since we are focusing on the elements, let's not
 distract ourselves with the [ordering invariant](#orderedlists)
 and reuse plain old lists. See [this](http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/07/29/putting-things-in-order.lhs/)
 for how to specify and verify order with plain old lists.]
@@ -486,7 +486,7 @@ handles or system resources can create unpleasant leaks.
 For example, the [xmonad][xmonad] window manager creates a
 sophisticated *zipper* data structure to hold the list of
 active user windows and carefully maintains the invariant
-that that the zipper contains no duplicates. Next, lets see how to
+that that the zipper contains no duplicates. Next, let's see how to
 specify and verify this invariant using LiquidHaskell, first for
 lists, and then for a simplified zipper.
 

src/Tutorial_10_Case_Study_Associative_Maps.lhs

@@ -95,7 +95,7 @@ that tracks the set of keys stored in the map, in order to
 statically ensure the safety of lookups.
 
 \newthought{Types} First, we need a type for `Map`s. As usual,
-lets parameterize the type with `k` for the type of keys and
+let's parameterize the type with `k` for the type of keys and
 `v` for the type of values:
 
 ~~~~~{.spec}
@@ -160,7 +160,7 @@ Using Maps: Well Scoped Expressions
 -----------------------------------
 
 Rather than jumping into the *implementation* of the above `Map` API,
-lets write a *client* that uses `Map`s to implement an interpreter for
+let's write a *client* that uses `Map`s to implement an interpreter for
 a tiny language. In particular, we will use maps as an *environment*
 containing the values of *bound variables*, and we will use the refined
 API to ensure that *lookups never fail*, and hence, that well-scoped
@@ -351,11 +351,11 @@ Implementing Maps: Binary Search Trees {#lemmas}
 We just saw how easy it is to *use* the Associative
 Map [API](#mapapi) to ensure the safety of lookups,
 even though the `Map` has a "dynamically" generated
-set of keys. Next, lets see how we can *implement*
+set of keys. Next, let's see how we can *implement*
 a `Map` library that respects the API using
 [Binary Search Trees](#binarysearchtree)
 
-\newthought{Data Type} First, lets provide an
+\newthought{Data Type} First, let's provide an
 implementation of the hitherto abstract data
 type for `Map`. We shall use Binary Search Trees,
 wherein, at each `Node`, the `left` (resp. `right`)
@@ -424,7 +424,7 @@ set k' v' (Node k v l r)
 set k' v' Tip = Node k' v' Tip Tip
 \end{code}
 
-\newthought{Lookup} Next, lets write the `mem` function that returns
+\newthought{Lookup} Next, let's write the `mem` function that returns
 the value associated with a key `k'`. To do so we just compare `k'`
 with the root key, if they are equal, we return the binding, and
 otherwise we go down the `left` (resp. `right`) subtree if sought for
@@ -445,7 +445,7 @@ get'  _ Tip   = die  "Lookup Never Fails"
 \newthought{Unfortunately} the function above is *rejected*
 by LiquidHaskell. This is a puzzler (and a bummer!) because
 in fact it *is* correct. So what gives?
-Well, lets look at the error for the call `get' k' l`
+Well, let's look at the error for the call `get' k' l`
 
 ~~~~~{.liquiderror}
  src/07-case-study-associative-maps.lhs:411:25: Error: Liquid Type Mismatch
@@ -461,7 +461,7 @@ Well, lets look at the error for the call `get' k' l`
 ~~~~~
 
 \noindent LiquidHaskell is *unable* to deduce that the key `k'`
-definitely belongs in the `left` subtree `l`. Well, lets ask ourselves:
+definitely belongs in the `left` subtree `l`. Well, let's ask ourselves:
 *why* must `k'` belong in the left subtree? From the input, we know
 `HasKey k' m` i.e. that `k'` is *somewhere* in `m`.
 That is *one of* the following holds:

src/Tutorial_11_Case_Study_Pointers.lhs

@@ -77,7 +77,7 @@ HeartBleeds in Haskell
 \newthought{Modern Languages} like Haskell are ultimately built upon the
 foundation of `C`. Thus, implementation errors could open up unpleasant
 vulnerabilities that could easily slither past the type system and even
-code inspection. As a concrete example, lets look at a function that
+code inspection. As a concrete example, let's look at a function that
 uses the `ByteString` library to truncate strings:
 
 \begin{code}
@@ -134,14 +134,14 @@ a hierarchy of levels (i.e. modules). Here, we have three levels:
 
 \noindent Our strategy, as before, is to develop an *refined API* for
 each level such that errors at each level are prevented by using the typed
-interfaces for the lower levels. Next, lets see how this strategy lets us
+interfaces for the lower levels. Next, let's see how this strategy lets us
 safely manipulate pointers.
 
 Low-level Pointer API
 ---------------------
 
-To get started, lets look at the low-level pointer API that is
-offered by GHC and the run-time. First, lets see who the
+To get started, let's look at the low-level pointer API that is
+offered by GHC and the run-time. First, let's see who the
 *dramatis personae* are and how they might let heartbleeds in.
 Then we will see how to batten down the hatches with LiquidHaskell.
 
@@ -203,7 +203,7 @@ operation `plusPtr p off` which takes a pointer `p` an integer
 plusPtr :: Ptr a -> Int -> Ptr b
 ~~~~~
 
-\newthought{Example} That was rather dry; lets look at a concrete
+\newthought{Example} That was rather dry; let's look at a concrete
 example of how one might use the low-level API. The following
 function allocates a block of 4 bytes and fills it with zeros:
 
@@ -437,7 +437,7 @@ but that is outside the scope of LiquidHaskell.]
 ByteString API
 --------------
 
-Next, lets see how the low-level API can be used to implement
+Next, let's see how the low-level API can be used to implement
 to implement [ByteStrings][bytestring], in a way that lets us
 perform fast string operations without opening the door to
 overflows.
@@ -490,7 +490,7 @@ to the legality requirements that the start and end of the `ByteString`
 be *within* the block of memory referred to by `bPtr`.
 
 
-\newthought{For brevity} lets define an alias for `ByteString`s of
+\newthought{For brevity} let's define an alias for `ByteString`s of
 a given size:
 
 \begin{code}
@@ -700,7 +700,7 @@ How *big* is the output list in terms of `p`, `n` and `acc`.
 Application API
 ---------------
 
-Finally, lets revisit our potentially "bleeding" `chop` function to
+Finally, let's revisit our potentially "bleeding" `chop` function to
 see how the refined `ByteString` API can prevent errors.  We require
 that the prefix size `n` be less than the size of the input string `s`:
 

src/Tutorial_12_Case_Study_AVL.lhs

@@ -139,7 +139,7 @@ Specifying AVL Trees
 --------------------
 
 The tricky bit is to ensure order and balance. Before we can ensure
-anything, lets tell LiquidHaskell what we mean by these terms, by
+anything, let's tell LiquidHaskell what we mean by these terms, by
 defining legal or valid AVL trees.
 
 \newthought{To Specify Order} we just define two aliases `AVLL` and `AVLR`
@@ -218,7 +218,7 @@ Smart Constructors
 ------------------
 
 Lets use the type to construct a few small trees which will
-also be handy in a general collection API. First, lets write
+also be handy in a general collection API. First, let's write
 an alias for trees of a given height:
 
 \begin{code}
@@ -282,7 +282,7 @@ the properties it requires and ensures.
 Inserting Elements
 ------------------
 
-Next, lets turn our attention to the problem of *adding* elements to
+Next, let's turn our attention to the problem of *adding* elements to
 an `AVL` tree. The basic strategy is this:
 
 1. *Find* the appropriate location (per ordering) to add the value,
@@ -624,7 +624,7 @@ insR = undefined
 Refactoring Rebalance
 ---------------------
 
-Next, lets write a function to `delete` an element from a tree.
+Next, let's write a function to `delete` an element from a tree.
 In general, we can apply the same strategy as `insert`:
 
 1. remove the element without worrying about heights,
@@ -639,7 +639,7 @@ is *inside* the `insL` which does the insertion as well.
 This is correct, but it means we would have to *repeat* the case
 analysis when deleting a value, which is unfortunate.
 
-\newthought{Instead lets refactor} the rebalancing code into a
+\newthought{Instead let's refactor} the rebalancing code into a
 separate function, that can be used by *both* `insert` and `delete`.
 It looks like this: