Adjust appends

exercises/practice/collatz-conjecture/.docs/instructions.append.md

@@ -30,6 +30,7 @@ In this exercise, the termination of the function is precisely the `collatz conj
 
 Consider using one of the following options:
 
-1. Adding the `partial` keyword before the declaration of the function disables termination checking and allows for (potentially unsafe) recursive calls.
+1. Adding the `partial` keyword before the declaration of a function disables termination checking and allows for (potentially unsafe) recursive calls.
 2. Imperative constructs allowed in monadic code, such as `while`, are implemented using partial recursion under the hood, so they can be used whenever termination is not enforced.
    Using the `Id` monad is a convenient way to enable these constructs in otherwise pure-looking code, without introducing additional effects.
+3. Defining a helper with an extra parameter for the maximum number of recursive calls ensures termination.

exercises/practice/high-scores/.docs/instructions.append.md

@@ -41,7 +41,11 @@ In general, updating an array in a functional setting requires copying the entir
 Lean uses reference counting to mitigate this drawback.
 As long as there is never more than one reference to an array (that is, it is used _linearly_), no copy is made and updates can be performed destructively.
 
-Lean also supports [do-notation][do-notation], an embedded language for writing code in an imperative style.
+Many functions in the `Array` API perform destructive updates in case of unshared data, for example, `set` and `push`.
+
+### Do-Notation
+
+Lean supports [do-notation][do-notation], an embedded language for writing code in an imperative style.
 
 Inside a `do` block, it is possible to declare mutable local variables, which can be reassigned, using the `mut` keyword.
 When used with data structures such as arrays, this allows Lean's runtime system to perform in-place destructive updates under the hood, whenever it is safe to do so.
@@ -50,7 +54,7 @@ Do-notation can only be used inside a monad.
 A convenient way to write imperative-style code that remains pure and has no observable side effects is to use the [Identity monad][id]:
 
 ```lean
-def function (array : Array Nat) := Id.run do
+def sumArray (array : Array Nat) := Id.run do
     let mut sum := 0
     for element in array do
         sum := sum + element

exercises/practice/kindergarten-garden/.docs/instructions.append.md

@@ -0,0 +1,20 @@
+# Instructions append
+
+## Vectors
+
+The return value of the `plants` function is a `Vector Plant 4`.
+
+Vectors represent arrays with a fixed length.
+This length may also be determined at runtime.
+They can be thought of as a pair consisting of an `Array` and a proof that the array has the required length.
+This means that you must provide this proof in order to construct a `Vector`.
+
+[This chapter][introduction] provides a good introduction to theorem proving in Lean.
+For a deeper dive, [this book][advanced] is listed as an official resource on the Lean website.
+
+Lean offers many tactics that can automate a proof or parts of it. 
+You might want to check a [language reference][reference].
+
+[introduction]: https://lean-lang.org/functional_programming_in_lean/Programming___-Proving___-and-Performance/
+[advanced]: https://lean-lang.org/theorem_proving_in_lean4/
+[reference]: https://lean-lang.org/doc/reference/latest/Tactic-Proofs/#tactics