From 0b13a7366fb583650d8debc1790f9ae01e9e07cd Mon Sep 17 00:00:00 2001 From: oxe-i Date: Tue, 10 Mar 2026 07:42:02 -0300 Subject: [PATCH 1/2] add append to kindergarten-garden, adjust append for collatz-conjecture and high-scores --- .../.docs/instructions.append.md | 3 ++- .../high-scores/.docs/instructions.append.md | 8 ++++++-- .../.docs/instructions.append.md | 19 +++++++++++++++++++ 3 files changed, 27 insertions(+), 3 deletions(-) create mode 100644 exercises/practice/kindergarten-garden/.docs/instructions.append.md diff --git a/exercises/practice/collatz-conjecture/.docs/instructions.append.md b/exercises/practice/collatz-conjecture/.docs/instructions.append.md index d062520..6f79285 100644 --- a/exercises/practice/collatz-conjecture/.docs/instructions.append.md +++ b/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. diff --git a/exercises/practice/high-scores/.docs/instructions.append.md b/exercises/practice/high-scores/.docs/instructions.append.md index baca5f1..c2546e0 100644 --- a/exercises/practice/high-scores/.docs/instructions.append.md +++ b/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 diff --git a/exercises/practice/kindergarten-garden/.docs/instructions.append.md b/exercises/practice/kindergarten-garden/.docs/instructions.append.md new file mode 100644 index 0000000..2c885d8 --- /dev/null +++ b/exercises/practice/kindergarten-garden/.docs/instructions.append.md @@ -0,0 +1,19 @@ +# Instructions append + +## Vectors + +The return value to the `plants` function is a `Vector Plant 4`. + +Vectors represent arrays with a fixed-length, which can be a runtime value. +They can be thought of as a pair consisting of an underlying `Array` and a proof that this `Array` has the necessary 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 [reference][reference] for the language. + +[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 From 6f0f0a0440ed3ff680ebd813c2291c5e3920b9f8 Mon Sep 17 00:00:00 2001 From: oxe-i Date: Tue, 10 Mar 2026 07:52:58 -0300 Subject: [PATCH 2/2] minor tweaks to kindergarten-garden append --- .../kindergarten-garden/.docs/instructions.append.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/exercises/practice/kindergarten-garden/.docs/instructions.append.md b/exercises/practice/kindergarten-garden/.docs/instructions.append.md index 2c885d8..23a43a1 100644 --- a/exercises/practice/kindergarten-garden/.docs/instructions.append.md +++ b/exercises/practice/kindergarten-garden/.docs/instructions.append.md @@ -2,17 +2,18 @@ ## Vectors -The return value to the `plants` function is a `Vector Plant 4`. +The return value of the `plants` function is a `Vector Plant 4`. -Vectors represent arrays with a fixed-length, which can be a runtime value. -They can be thought of as a pair consisting of an underlying `Array` and a proof that this `Array` has the necessary length. +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 [reference][reference] for the language. +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/