merge

extra/extra/Logic.lagda

@@ -301,7 +301,7 @@ evidence that a disjunction holds.
 We set the precedence of disjunction so that it binds less tightly
 than any other declared operator.
 \begin{code}
-infix 1 _⊎_
+infixr 1 _⊎_
 \end{code}
 Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
 

src/plfa/part1/Connectives.lagda.md

@@ -389,7 +389,7 @@ simplify to the same term, and similarly for `inj₂ y`.
 We set the precedence of disjunction so that it binds less tightly
 than any other declared operator:
 ```
-infix 1 _⊎_
+infixr 1 _⊎_
 ```
 Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
 

src/plfa/part1/Lists.lagda.md

@@ -115,12 +115,11 @@ _++_ : ∀ {A : Set} → List A → List A → List A
 []       ++ ys  =  ys
 (x ∷ xs) ++ ys  =  x ∷ (xs ++ ys)
 ```
-The type `A` is an implicit argument to append, making it a
+The type `A` is an implicit argument to append, making it a _polymorphic_
-_polymorphic_ function (one that can be used at many types).  The
+function (one that can be used at many types). A list appended to the empty list
-empty list appended to another list yields the other list.  A
+yields the list itself. A list appended to a non-empty list yields a list with
-non-empty list appended to another list yields a list with head the
+the head the same as the head of the non-empty list, and a tail the same as the
-same as the head of the first list and tail the same as the tail of
+other list appended to tail of the non-empty list.
-the first list appended to the second list.
 
 Here is an example, showing how to compute the result
 of appending two lists: