From cd4014e02ced3241dab15414e79e88a209c8a09b Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 12:52:56 +0100
Subject: [PATCH 01/27] Switch to partial fixpoint pr-release

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 62ccd71..12fc5b0 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc1
+leanprover/lean4-pr-releases:pr-release-6355

From 212d52d2eb3c6c7d9bd0b76c29fc21fd0ce20361 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 13:48:03 +0100
Subject: [PATCH 02/27] Reapply "Local setup"

This reverts commit 7a0ee068c8ca593835ddfca42d3b1f363d80a500.
---
 .envrc     |  1 +
 flake.lock | 27 +++++++++++++++++++++++++++
 flake.nix  | 15 +++++++++++++++
 3 files changed, 43 insertions(+)
 create mode 100644 .envrc
 create mode 100644 flake.lock
 create mode 100644 flake.nix

diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000..3550a30
--- /dev/null
+++ b/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..6f885a8
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,27 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1736243181,
+        "narHash": "sha256-yaAZO4ttZ3q9/U0zFVtzpVGO6B8+DMpshnF1+0E5Kkg=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "8bcd7d056d69e2e6c47ddf40c2c401cb173c0d67",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "master",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..d9fb84b
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,15 @@
+{
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs/master";
+  outputs = { self, nixpkgs }:
+    let
+      system = "x86_64-linux";
+      pkgs = import nixpkgs { inherit system; };
+    in
+    { devShell.${system} = pkgs.stdenv.mkDerivation rec {
+      name = "env";
+      buildInputs = with pkgs; [
+        elan
+        python3
+      ];
+   };};
+}

From 168a53b01387eaaad042d03e3e3908ab6cd21f45 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 18:18:39 +0100
Subject: [PATCH 03/27] A bit more

---
 Manual/Language/RecursiveDefs.lean            |  14 +-
 .../RecursiveDefs/PartialFixpoint.lean        | 270 ++++++++++++++++++
 2 files changed, 283 insertions(+), 1 deletion(-)
 create mode 100644 Manual/Language/RecursiveDefs/PartialFixpoint.lean

diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean
index 777ea56..f8e8fa5 100644
--- a/Manual/Language/RecursiveDefs.lean
+++ b/Manual/Language/RecursiveDefs.lean
@@ -9,6 +9,7 @@ import VersoManual
 import Manual.Meta
 
 import Manual.Language.RecursiveDefs.Structural
+import Manual.Language.RecursiveDefs.PartialFixpoint
 
 open Verso.Genre Manual
 open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
@@ -29,7 +30,7 @@ Furthermore, most useful recursive functions do not threaten soundness, and infi
 Instead of banning recursive functions, Lean requires that each recursive function is defined safely.
 While elaborating recursive definitions, the Lean elaborator also produces a justification that the function being defined is safe.{margin}[The section on {ref "elaboration-results"}[the elaborator's output] in the overview of elaboration contextualizes the elaboration of recursive definitions in the overall context of the elaborator.]
 
-There are four main kinds of recursive functions that can be defined:
+There are five main kinds of recursive functions that can be defined:
 
 : Structurally recursive functions
 
@@ -47,6 +48,15 @@ There are four main kinds of recursive functions that can be defined:
   Applications of functions defined via well-founded recursion are not necessarily definitionally equal to their return values, but this equality can be proved as a proposition.
   Even when definitional equalities exist, these functions are frequently slow to compute with because they require reducing proof terms that are often very large.
 
+: Recursive functions as fixpoints
+
+  Taking the function definition as an equation that specifies the behavior of the function, in
+  certain cases the existence of a function satisfying this specification can be proven. This stategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_.
+
+  In particular monadic functions in certain monads (e.g. {name}`Option`) are amenable for this strategy, and additional theorems are generated by lean (partial correctness).
+
+  As with well-founded recursion, applications of functions defined via partial fixpoint are not definitially equal to their return values.
+
 : Partial functions with nonempty ranges
 
   For many applications, it's not important to reason about the implementation of certain functions.
@@ -162,6 +172,8 @@ tag := "well-founded-recursion"
 This section will describe the translation of {deftech}[well-founded recursion].
 :::
 
+{include 0 Manual.Language.RecursiveDefs.PartialFixpoint}
+
 # Partial and Unsafe Recursive Definitions
 %%%
 tag := "partial-unsafe"
diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
new file mode 100644
index 0000000..16e9ba6
--- /dev/null
+++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
@@ -0,0 +1,270 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Joachim Breitner
+-/
+
+import VersoManual
+
+import Manual.Meta
+
+open Manual
+open Verso.Genre
+open Verso.Genre.Manual
+open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
+
+#doc (Manual) "Partial Fixpoint Recursion" =>
+%%%
+tag := "partial-fixpoint"
+%%%
+
+A function definition can be understood as a request to Lean to construct a function of the given type that satisfies the given equation.
+One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {tech}[well-founded recursion] is to guarantee the existence and uniqueness the constructued functions.
+
+In some cases, the equation may not uniquely determine the function's (extensional) behavior, because it
+does not terminate for all arguments in the above sense, but there still exist functions for which the defining equation holds.
+In these cases, a definition by {deftech}_partial fixpoint_ may be possible.
+
+Even in cases where the defining equation fully describes the function's behavior and a termination proof using {tech}[well-founded recursion] would be possible it may simply be more convenient to define the function using partial fixpoint, to avoid a possible tedious termination proof.
+
+Definition by partial fixpoint is only used when explicitly requested by the user, by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`.
+
+There are two classes of functions for which a definition by partial fixpoint work:
+
+* tail-recursive functions of inhabited type, and
+* monadic functions in a suitable monad, such as the {name}`Option` monad.
+
+Both classes are backed by the same theory and construction: least fixpoints of monotone equations in chain-complete partial orders.
+
+Lean supports {tech}[mutually recursive] functions to be defined by partial fixpoint.
+For this, every function definition in a mutual block has to be annotated with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`.
+
+:::example "Definition by Partial Fixpoint"
+
+The following function find the least natural number for which the predicate `p` holds.
+If `p` never holds then this equation does not specify the behavior: the function `find` could return 42 in that case, and still satisfy the equation.
+
+```lean (keep := false)
+def find (p : Nat → Bool) (i : Nat := 0) : Nat :=
+  if p i then
+    i
+  else
+    find p (i + 1)
+partial_fixpoint
+```
+
+The elaborator can prove that functions satisfying the equation exist, and defined `find` to be an arbitrary such function.
+:::
+
+# Tail-recursive functions
+%%%
+tag := "partial-fixpoint-tailrec"
+%%%
+
+Definition by partial fixpoint will succeed if the following two conditoins hold:
+
+1. The function's type is inhabited (as with {ref "partial-unsafe"}[functions marked {keywordOf Lean.Parser.Command.declaration}`partial`]).
+2. All recursive calls are in {tech}[tail position] of the function.
+
+A {deftech}_tail position_ of the function body is
+
+* the funcion body itself,
+* the branches of a {keywordOf Lean.Parser.Term.match}`match` expression in tail position,
+* the branches of an {keywordOf termIfThenElse}`if` expression in tail position, and
+* the body of a {keywordOf Lean.Parser.Term.let}`let` expression in tail position.
+
+In particular, the {tech key:="match discriminant"}[discriminant] of a {keywordOf Lean.Parser.Term.match}`match` expression, the condition of an {keywordOf termIfThenElse}`if` expression and the arguments of functions are not tail-positions.
+
+:::example "Tail recursive functions"
+
+Because the function body itself is a tail-position, clearly looping definitions are accepted:
+
+```lean (keep := false)
+def loop (x : Nat) : Nat := loop (x + 1)
+partial_fixpoint
+```
+
+More useful function definitions tend to have some branching.
+The following example can also be constructed using well-founded recursion with a termination proof, but may be more convenient to define using  {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`.
+
+```lean (keep := false)
+def Array.find (xs : Array α) (p : α → Bool) (i : Nat := 0) : Option α :=
+  if h : i < xs.size then
+    if p xs[i] then
+      some xs[i]
+    else
+      Array.find xs p (i + 1)
+  else
+    none
+partial_fixpoint
+```
+
+If the result of the recursive call is not just returned, but passed to another function, it is not in tail position and this definition fails.
+
+```lean (keep := false) (error := true) (name := nonTailPos)
+def List.findIndex (xs : List α) (p : α → Bool) : Int := match xs with
+  | [] => -1
+  | x::ys =>
+    if p x then
+      0
+    else
+      let r := List.findIndex ys p
+      if r = -1 then -1 else r + 1
+partial_fixpoint
+```
+```leanOutput nonTailPos
+Could not prove 'List.findIndex' to be monotone in its recursive calls:
+  Cannot eliminate recursive call `List.findIndex ys p` enclosed in
+    let r := ys✝.findIndex p;
+    if r = -1 then -1 else r + 1
+```
+
+:::
+
+# Monadic functions
+%%%
+tag := "partial-fixpoint-monadic"
+%%%
+
+
+Definition by partial fixpoint is more powerful if the function's type is monadic, the monad is an instance of {name}`Lean.Order.MonoBind` (such as {name}`Option`).
+In this case, recursive call are not restricted to tail-positions, but can also be inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`.
+
+The set of higher-order functions for which this works is extensible (see TODO below), so no exhaustive list is given here.
+The aspiration is that a monadic recursive function definition that is built using abstract monadic operations like {name}`bind`, but not open the abstraction of the monad (e.g. by matching on the {name}`Option` value), is accepted.
+In particular, using {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation] should work.
+
+:::example "Monadic functions"
+
+The following function implements the Ackermann function in the {name}`Option` monad, and is accepted without a (explicit or implicit) termination proof:
+
+```lean (keep := false)
+def ack : (n m : Nat) → Option Nat
+  | 0,   y   => some (y+1)
+  | x+1, 0   => ack x 1
+  | x+1, y+1 => do ack x (← ack (x+1) y)
+partial_fixpoint
+```
+
+Recursion can also happen within higher-order library functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]:
+
+```lean (keep := false)
+structure Tree where cs : List Tree
+
+def Tree.rev (t : Tree) : Option Tree := do
+  Tree.mk (← t.cs.reverse.mapM (Tree.rev ·))
+partial_fixpoint
+
+def Tree.rev' (t : Tree) : Option Tree := do
+  let mut cs := []
+  for c in t.cs do
+    cs := (← c.rev') :: cs
+  return Tree.mk cs
+partial_fixpoint
+```
+
+Pattern matching on the result of the recursive call will prevent the definition by partial fixpoint to go through:
+
+```lean (keep := false) (error := true) (name := monoMatch)
+def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with
+  | [] => none
+  | x::ys =>
+    if p x then
+      some 0
+    else
+      match List.findIndex ys p with
+      | none => none
+      | some r => some (r + 1)
+partial_fixpoint
+```
+```leanOutput monoMatch
+Could not prove 'List.findIndex' to be monotone in its recursive calls:
+  Cannot eliminate recursive call `List.findIndex ys p` enclosed in
+    match ys✝.findIndex p with
+    | none => none
+    | some r => some (r + 1)
+```
+
+In this particular case, using the {name}`Functor.map` function instead of explicit pattern matching helps:
+
+```lean
+def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with
+  | [] => none
+  | x::ys =>
+    if p x then
+      some 0
+    else
+      (· + 1) <$> List.findIndex ys p
+partial_fixpoint
+```
+:::
+
+# Partial Correctnes Theorem
+%%%
+tag := "partial-correctness-theorem"
+%%%
+
+In general, for funcitons defined by partial fixpoint we know obtain the equational theorems that prove that the function indeed satisfies the given equation, and enables proofs by rewriting.
+But these do not allow reasoning about the behavior of the function on the underspecified arguments.
+
+If the monad happens to be the {name}`Option` monad, then by construction the function equals {name}`Option.none` on all function inputs for which the defining equation is not terminating.
+From this fact, Lean proves a {deftech}_partial correctness theorem_ for the function which allows concluding facts from the function's result being {name}`Option.some`.
+
+
+:::example "Partial correctness theorem"
+
+Recall this function from an earlier example:
+
+```lean
+def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with
+  | [] => none
+  | x::ys =>
+    if p x then
+      some 0
+    else
+      (· + 1) <$> List.findIndex ys p
+partial_fixpoint
+```
+
+For this function definition, Lean proves the following partial correctness theorem:
+
+```signature
+List.findIndex.partial_correctness {α : Type _} (motive : List α → (α → Bool) → Nat → Prop)
+  (h :
+    ∀ (findIndex : List α → (α → Bool) → Option Nat),
+      (∀ (xs : List α) (p : α → Bool) (r : Nat), findIndex xs p = some r → motive xs p r) →
+        ∀ (xs : List α) (p : α → Bool) (r : Nat),
+          (match xs with
+              | [] => none
+              | x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys p) =
+              some r →
+            motive xs p r)
+  (xs : List α) (p : α → Bool) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs p r✝
+```
+
+We can use this theorem to prove that the resulting number is a valid index in the list and that the predicate holds for that index:
+
+```lean
+theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) :
+    xs.findIndex p = some i → xs[i]?.any p := by
+  apply List.findIndex.partial_correctness (motive := fun xs p i => xs[i]?.any p)
+  intro findIndex ih xs p r hsome
+  split at hsome
+  next => contradiction
+  next x ys =>
+    split at hsome
+    next =>
+      have : r = 0 := by simp_all
+      simp_all
+    next =>
+      simp only [Option.map_eq_map, Option.map_eq_some'] at hsome
+      obtain ⟨r', hr, rfl⟩ := hsome
+      specialize ih _ _ _ hr
+      simpa
+```
+
+:::
+
+# Theory and Construction
+
+TODO

From 3fd2703c8a973dc01101010a6dd53833ad7faaf8 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 18:19:51 +0100
Subject: [PATCH 04/27] 5

---
 Manual/Language/RecursiveDefs.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean
index f8e8fa5..3ef8d78 100644
--- a/Manual/Language/RecursiveDefs.lean
+++ b/Manual/Language/RecursiveDefs.lean
@@ -87,7 +87,7 @@ As described in the {ref "elaboration-results"}[overview of the elaborator's out
     If there is no such clause, then the elaborator performs a search, testing each parameter to the function as a candidate for structural recursion, and attempting to find a measure with a well-founded relation that decreases at each recursive call.
 
 This section describes the rules that govern recursive functions.
-After a description of mutual recursion, each of the four kinds of recursive definitions is specified, along with the tradeoffs between reasoning power and flexibility that go along with each.
+After a description of mutual recursion, each of the five kinds of recursive definitions is specified, along with the tradeoffs between reasoning power and flexibility that go along with each.
 
 # Mutual Recursion
 %%%

From 59287ee88c70d4e4e2bd58aa8cf468dbab7b72d0 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 18:48:14 +0100
Subject: [PATCH 05/27] fixes

---
 Manual/Language/RecursiveDefs/PartialFixpoint.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
index 16e9ba6..689b73b 100644
--- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
@@ -108,14 +108,14 @@ def List.findIndex (xs : List α) (p : α → Bool) : Int := match xs with
     if p x then
       0
     else
-      let r := List.findIndex ys p
+      have r := List.findIndex ys p
       if r = -1 then -1 else r + 1
 partial_fixpoint
 ```
 ```leanOutput nonTailPos
 Could not prove 'List.findIndex' to be monotone in its recursive calls:
   Cannot eliminate recursive call `List.findIndex ys p` enclosed in
-    let r := ys✝.findIndex p;
+    let_fun r := ys✝.findIndex p;
     if r = -1 then -1 else r + 1
 ```
 
@@ -228,7 +228,9 @@ partial_fixpoint
 
 For this function definition, Lean proves the following partial correctness theorem:
 
-```signature
+{TODO}[using `signature` causes max recursion error]
+
+```
 List.findIndex.partial_correctness {α : Type _} (motive : List α → (α → Bool) → Nat → Prop)
   (h :
     ∀ (findIndex : List α → (α → Bool) → Option Nat),
@@ -239,7 +241,7 @@ List.findIndex.partial_correctness {α : Type _} (motive : List α → (α → B
               | x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys p) =
               some r →
             motive xs p r)
-  (xs : List α) (p : α → Bool) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs p r✝
+  (xs : List α) (p : α → Bool) (r : Nat) : xs.findIndex p = some r → motive xs p r
 ```
 
 We can use this theorem to prove that the resulting number is a valid index in the list and that the predicate holds for that index:

From 3c61ae90650febadb06acb4f088eb3d1ed295448 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 18:51:25 +0100
Subject: [PATCH 06/27] Shorter lines

---
 Manual/Language/RecursiveDefs/PartialFixpoint.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
index 689b73b..c9d37d8 100644
--- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
@@ -102,7 +102,8 @@ partial_fixpoint
 If the result of the recursive call is not just returned, but passed to another function, it is not in tail position and this definition fails.
 
 ```lean (keep := false) (error := true) (name := nonTailPos)
-def List.findIndex (xs : List α) (p : α → Bool) : Int := match xs with
+def List.findIndex (xs : List α) (p : α → Bool) : Int :=
+  match xs with
   | [] => -1
   | x::ys =>
     if p x then
@@ -166,7 +167,8 @@ partial_fixpoint
 Pattern matching on the result of the recursive call will prevent the definition by partial fixpoint to go through:
 
 ```lean (keep := false) (error := true) (name := monoMatch)
-def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with
+def List.findIndex (xs : List α) (p : α → Bool) : Option Nat :=
+  match xs with
   | [] => none
   | x::ys =>
     if p x then
@@ -188,7 +190,8 @@ Could not prove 'List.findIndex' to be monotone in its recursive calls:
 In this particular case, using the {name}`Functor.map` function instead of explicit pattern matching helps:
 
 ```lean
-def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with
+def List.findIndex (xs : List α) (p : α → Bool) : Option Nat :=
+  match xs with
   | [] => none
   | x::ys =>
     if p x then
@@ -216,7 +219,8 @@ From this fact, Lean proves a {deftech}_partial correctness theorem_ for the fun
 Recall this function from an earlier example:
 
 ```lean
-def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with
+def List.findIndex (xs : List α) (p : α → Bool) : Option Nat :=
+  match xs with
   | [] => none
   | x::ys =>
     if p x then

From cce70f53485396dcf9fd959df66ab78f1b7cbdd3 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 18:58:23 +0100
Subject: [PATCH 07/27] Copy editing

---
 Manual/Language/RecursiveDefs/PartialFixpoint.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
index c9d37d8..b2ddb4a 100644
--- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
@@ -128,7 +128,7 @@ tag := "partial-fixpoint-monadic"
 %%%
 
 
-Definition by partial fixpoint is more powerful if the function's type is monadic, the monad is an instance of {name}`Lean.Order.MonoBind` (such as {name}`Option`).
+Definition by partial fixpoint is more powerful if the function's type is monadic and the monad is an instance of {name}`Lean.Order.MonoBind`, such as {name}`Option`.
 In this case, recursive call are not restricted to tail-positions, but can also be inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`.
 
 The set of higher-order functions for which this works is extensible (see TODO below), so no exhaustive list is given here.
@@ -207,7 +207,7 @@ partial_fixpoint
 tag := "partial-correctness-theorem"
 %%%
 
-In general, for funcitons defined by partial fixpoint we know obtain the equational theorems that prove that the function indeed satisfies the given equation, and enables proofs by rewriting.
+In general, for functions defined by partial fixpoint we only obtain the equational theorems that prove that the function indeed satisfies the given equation, and enables proofs by rewriting.
 But these do not allow reasoning about the behavior of the function on the underspecified arguments.
 
 If the monad happens to be the {name}`Option` monad, then by construction the function equals {name}`Option.none` on all function inputs for which the defining equation is not terminating.
@@ -230,7 +230,7 @@ def List.findIndex (xs : List α) (p : α → Bool) : Option Nat :=
 partial_fixpoint
 ```
 
-For this function definition, Lean proves the following partial correctness theorem:
+With this function definition, Lean proves the following partial correctness theorem:
 
 {TODO}[using `signature` causes max recursion error]
 

From 3c3d32ef225dafc98dcc86fb9fbecf01df93b057 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 19:08:13 +0100
Subject: [PATCH 08/27] Typos

---
 .vale/styles/config/ignore/terms.txt               | 2 ++
 Manual/Language/RecursiveDefs.lean                 | 6 +++---
 Manual/Language/RecursiveDefs/PartialFixpoint.lean | 8 ++++----
 3 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt
index fdc93e8..e259355 100644
--- a/.vale/styles/config/ignore/terms.txt
+++ b/.vale/styles/config/ignore/terms.txt
@@ -1,5 +1,6 @@
 APIs
 Abelian
+Ackermann
 Kleisli
 Packrat
 antiquotation
@@ -49,6 +50,7 @@ enum
 equational
 extensional
 extensionality
+fixpoint
 functor
 functor's
 functors
diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean
index 3ef8d78..2ffe914 100644
--- a/Manual/Language/RecursiveDefs.lean
+++ b/Manual/Language/RecursiveDefs.lean
@@ -50,12 +50,12 @@ There are five main kinds of recursive functions that can be defined:
 
 : Recursive functions as fixpoints
 
-  Taking the function definition as an equation that specifies the behavior of the function, in
-  certain cases the existence of a function satisfying this specification can be proven. This stategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_.
+  Taking the function definition as an equation that specifies the behavior of the function, in certain cases the existence of a function satisfying this specification can be proven.
+  This stategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_.
 
   In particular monadic functions in certain monads (e.g. {name}`Option`) are amenable for this strategy, and additional theorems are generated by lean (partial correctness).
 
-  As with well-founded recursion, applications of functions defined via partial fixpoint are not definitially equal to their return values.
+  As with well-founded recursion, applications of functions defined via partial fixpoint are not definitionally equal to their return values.
 
 : Partial functions with nonempty ranges
 
diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
index b2ddb4a..3888270 100644
--- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
@@ -19,7 +19,7 @@ tag := "partial-fixpoint"
 %%%
 
 A function definition can be understood as a request to Lean to construct a function of the given type that satisfies the given equation.
-One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {tech}[well-founded recursion] is to guarantee the existence and uniqueness the constructued functions.
+One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {tech}[well-founded recursion] is to guarantee the existence and uniqueness the constructed functions.
 
 In some cases, the equation may not uniquely determine the function's (extensional) behavior, because it
 does not terminate for all arguments in the above sense, but there still exist functions for which the defining equation holds.
@@ -61,7 +61,7 @@ The elaborator can prove that functions satisfying the equation exist, and defin
 tag := "partial-fixpoint-tailrec"
 %%%
 
-Definition by partial fixpoint will succeed if the following two conditoins hold:
+Definition by partial fixpoint will succeed if the following two conditions hold:
 
 1. The function's type is inhabited (as with {ref "partial-unsafe"}[functions marked {keywordOf Lean.Parser.Command.declaration}`partial`]).
 2. All recursive calls are in {tech}[tail position] of the function.
@@ -202,13 +202,13 @@ partial_fixpoint
 ```
 :::
 
-# Partial Correctnes Theorem
+# Partial Correctness Theorem
 %%%
 tag := "partial-correctness-theorem"
 %%%
 
 In general, for functions defined by partial fixpoint we only obtain the equational theorems that prove that the function indeed satisfies the given equation, and enables proofs by rewriting.
-But these do not allow reasoning about the behavior of the function on the underspecified arguments.
+But these do not allow reasoning about the behavior of the function on arguments for which the function specification does not terminate.
 
 If the monad happens to be the {name}`Option` monad, then by construction the function equals {name}`Option.none` on all function inputs for which the defining equation is not terminating.
 From this fact, Lean proves a {deftech}_partial correctness theorem_ for the function which allows concluding facts from the function's result being {name}`Option.some`.

From fe2a45b8a3541b48278807fbf2129511e2b1fd10 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 19:21:19 +0100
Subject: [PATCH 09/27] More typos

---
 .vale/styles/config/ignore/terms.txt | 1 +
 Manual/Language/RecursiveDefs.lean   | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt
index e259355..7bcb040 100644
--- a/.vale/styles/config/ignore/terms.txt
+++ b/.vale/styles/config/ignore/terms.txt
@@ -51,6 +51,7 @@ equational
 extensional
 extensionality
 fixpoint
+fixpoints
 functor
 functor's
 functors
diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean
index 2ffe914..b1e9ddd 100644
--- a/Manual/Language/RecursiveDefs.lean
+++ b/Manual/Language/RecursiveDefs.lean
@@ -51,7 +51,7 @@ There are five main kinds of recursive functions that can be defined:
 : Recursive functions as fixpoints
 
   Taking the function definition as an equation that specifies the behavior of the function, in certain cases the existence of a function satisfying this specification can be proven.
-  This stategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_.
+  This strategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_.
 
   In particular monadic functions in certain monads (e.g. {name}`Option`) are amenable for this strategy, and additional theorems are generated by lean (partial correctness).
 

From 1b8706874479762d240877b091cf2bc04f78133e Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Jan 2025 21:28:49 +0100
Subject: [PATCH 10/27] Even more typos

---
 Manual/Language/RecursiveDefs/PartialFixpoint.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
index 3888270..fe54433 100644
--- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
@@ -68,7 +68,7 @@ Definition by partial fixpoint will succeed if the following two conditions hold
 
 A {deftech}_tail position_ of the function body is
 
-* the funcion body itself,
+* the function body itself,
 * the branches of a {keywordOf Lean.Parser.Term.match}`match` expression in tail position,
 * the branches of an {keywordOf termIfThenElse}`if` expression in tail position, and
 * the body of a {keywordOf Lean.Parser.Term.let}`let` expression in tail position.

From ccdb638e34e69f6c7b91a16e8bc70057b624dceb Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 17 Jan 2025 16:41:50 +0100
Subject: [PATCH 11/27] More on theory

---
 .../RecursiveDefs/PartialFixpoint.lean        | 78 ++++++++++++++++++-
 Manual/Meta/Monotonicity.lean                 | 75 ++++++++++++++++++
 2 files changed, 151 insertions(+), 2 deletions(-)
 create mode 100644 Manual/Meta/Monotonicity.lean

diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
index fe54433..69507c4 100644
--- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
@@ -7,12 +7,15 @@ Author: Joachim Breitner
 import VersoManual
 
 import Manual.Meta
+import Manual.Meta.Monotonicity
 
 open Manual
 open Verso.Genre
 open Verso.Genre.Manual
 open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
 
+open Lean.Order
+
 #doc (Manual) "Partial Fixpoint Recursion" =>
 %%%
 tag := "partial-fixpoint"
@@ -29,7 +32,7 @@ Even in cases where the defining equation fully describes the function's behavio
 
 Definition by partial fixpoint is only used when explicitly requested by the user, by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`.
 
-There are two classes of functions for which a definition by partial fixpoint work:
+There are two classes of functions for which a definition by partial fixpoint works:
 
 * tail-recursive functions of inhabited type, and
 * monadic functions in a suitable monad, such as the {name}`Option` monad.
@@ -272,5 +275,76 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) :
 :::
 
 # Theory and Construction
+%%%
+tag := "partial-fixpoint-theory"
+%%%
+
+The construction builds on a variant of the Knaster–Tarski theorem: In a chain-complete partial order, every monotone function has a least fixed point.
+
+The necessary theory is found in the `Lean.Order` namespace.
+This is not meant to be a general purpose library of order theoretic results.
+Instead, the definitions and theorems therein are only intended to back the
+{keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` feature.
+
+The notion of a partial order, and that of a chain-complete partial order, are represented as type classes:
+
+{docstring Lean.Order.PartialOrder}
+
+{docstring Lean.Order.CCPO}
+
+The fixpoint of a monotone function can be taken using {name}`fix`, which indeed constructs a fixpoint, as shown by {name}`fix_eq`,
+
+{docstring Lean.Order.fix}
+
+{docstring Lean.Order.fix_eq}
+
+So to construct the function, Lean first infers a suitable {name}`CCPO` instance.
+
+```lean (show := false)
+section
+universe u v
+variable (α : Type u)
+variable (β : α → Sort v) [∀ x, CCPO (β x)]
+variable (w : α)
+```
+
+* If the function's result type has a dedicated instance, like {name}`Option` has with {inst}`CCPO (Option α)`, this is used together with the instance for the function type, {inst}`CCPO (∀ x, β x)`, to construct an instance for the whole function's type.
+
+* Else, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {inst}`CCPO (FlatOrder w)` is used, `w` is a least element and all other elements are incomparable.
 
-TODO
+```lean (show := false)
+end
+```
+
+Next, the recursive calls in the right-hand side of the function definitions are abstracted; this turns into the argument `f` of {name}`fix`. The monotonicity requirement is solved by the {tactic}`monotonicity` tactic, which applies compositional monotonicity lemmas in a syntax-driven way
+
+The tactic solves goals of the form `monotone (fun x => …)` using the following steps:
+
+* Applying {name}`monotone_const` when there is no dependency on `x` left.
+* Splitting on {keywordOf Lean.Parser.Term.match}`match` expressions.
+* Splitting on {keywordOf termIfThenElse}`if` expressions.
+* Moving {keywordOf Lean.Parser.Term.let}`let` expression to the context, if the value and type do not depend on `x`.
+* Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on `x`.
+* Applying lemmas annotated with {attr}`partial_fixpoint_monotone`
+
+:::example "List of Monotonicity Lemmas"
+
+::::TODO
+Not really an example, but probably better to have this collapsible?
+::::
+
+The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function:
+
+::::TODO
+
+What I’d like to see here is
+
+* {name}`Lean.Order.monotone_array_allM`: applies to `List.mapM ⬝ _`
+
+where I use `·` and `_` to distinguish the monotone arguments from others.
+
+::::
+
+{monotonicityLemmas}
+
+:::
diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
new file mode 100644
index 0000000..e62d00e
--- /dev/null
+++ b/Manual/Meta/Monotonicity.lean
@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Joachim Breitner
+-/
+
+import Lean.Elab.Command
+import Lean.Elab.InfoTree
+
+import Verso
+import Verso.Doc.ArgParse
+import Verso.Doc.Elab.Monad
+import VersoManual
+import Verso.Code
+
+import SubVerso.Highlighting
+import SubVerso.Examples
+
+import Manual.Meta.Attribute
+import Manual.Meta.Basic
+import Manual.Meta.Bibliography
+import Manual.Meta.CustomStyle
+import Manual.Meta.Example
+import Manual.Meta.Figure
+import Manual.Meta.Lean
+import Manual.Meta.Lean.IO
+import Manual.Meta.Marginalia
+import Manual.Meta.ParserAlias
+import Manual.Meta.Syntax
+import Manual.Meta.Table
+import Manual.Meta.Tactics
+import Manual.Meta.SpliceContents
+
+open Lean Meta Elab
+open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
+open SubVerso.Highlighting Highlighted
+
+open Lean.Elab.Tactic.GuardMsgs
+
+namespace Manual
+
+@[block_role_expander monotonicityLemmas]
+def monotonicityLemmas : BlockRoleExpander
+  | #[], #[] => do
+    let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values
+    let names := names.qsort (toString · < toString ·)
+
+    let itemStx : TSyntaxArray `term ← names.mapM fun name => do
+      -- Extract the target pattern
+      let ci ← getConstInfo name
+      let targetStx : TSyntax `term ←
+        forallTelescope ci.type fun _ concl => do
+          unless concl.isAppOfArity ``Lean.Order.monotone 5 do
+            throwError "Unexpecte conclusion of {name}"
+          let f := concl.appArg!
+          unless f.isLambda do
+            throwError "Unexpecte conclusion of {name}"
+          lambdaBoundedTelescope f 1 fun _ _call => do
+            -- Could not get this to work:
+            -- let _stx ← Lean.PrettyPrinter.delab call
+            -- `(Inline.code $(quote stx))
+            `(Inline.text "TODO")
+            -- pure (some stx)
+
+      let hl : Highlighted ← constTok name name.toString
+      let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)])
+      `(Verso.Doc.Block.para #[$nameStx, Inline.text ": applies to ", $targetStx])
+
+    let theList ← `(Verso.Doc.Block.ul #[$[⟨#[$itemStx]⟩],*])
+    return #[theList]
+  | _, _ => throwError "Unexpected arguments"
+
+-- #eval do
+--   let (ss, _) ← (monotonicityLemmas #[] #[]).run {} (.init .missing)
+--   logInfo (ss[0]!.raw.prettyPrint)

From 898660a89b358b3541f1b1e051d6071d18079cb7 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 17 Jan 2025 16:50:33 +0100
Subject: [PATCH 12/27] Render as plain text

---
 .../Language/RecursiveDefs/PartialFixpoint.lean   | 15 +++++++--------
 Manual/Meta/Monotonicity.lean                     | 11 +++++------
 2 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
index 69507c4..6f030a2 100644
--- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
@@ -327,14 +327,6 @@ The tactic solves goals of the form `monotone (fun x => …)` using the followin
 * Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on `x`.
 * Applying lemmas annotated with {attr}`partial_fixpoint_monotone`
 
-:::example "List of Monotonicity Lemmas"
-
-::::TODO
-Not really an example, but probably better to have this collapsible?
-::::
-
-The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function:
-
 ::::TODO
 
 What I’d like to see here is
@@ -345,6 +337,13 @@ where I use `·` and `_` to distinguish the monotone arguments from others.
 
 ::::
 
+:::example "List of Monotonicity Lemmas"
+
+{TODO}[Not really an example, but probably better to have this collapsible?]
+
+The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function:
+
+
 {monotonicityLemmas}
 
 :::
diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
index e62d00e..c547850 100644
--- a/Manual/Meta/Monotonicity.lean
+++ b/Manual/Meta/Monotonicity.lean
@@ -55,12 +55,11 @@ def monotonicityLemmas : BlockRoleExpander
           let f := concl.appArg!
           unless f.isLambda do
             throwError "Unexpecte conclusion of {name}"
-          lambdaBoundedTelescope f 1 fun _ _call => do
-            -- Could not get this to work:
-            -- let _stx ← Lean.PrettyPrinter.delab call
-            -- `(Inline.code $(quote stx))
-            `(Inline.text "TODO")
-            -- pure (some stx)
+          lambdaBoundedTelescope f 1 fun _ call => do
+            let stx ← Lean.PrettyPrinter.delab call
+            let format := Syntax.prettyPrint stx
+            let str := format.pretty'
+            `(Inline.code $(quote str))
 
       let hl : Highlighted ← constTok name name.toString
       let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)])

From e18cb0cea5e2adcee7ac7fceced7efe4c494e18f Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 17 Jan 2025 16:52:34 +0100
Subject: [PATCH 13/27] Less imports

---
 Manual/Meta/Monotonicity.lean | 23 +----------------------
 1 file changed, 1 insertion(+), 22 deletions(-)

diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
index c547850..0b75c28 100644
--- a/Manual/Meta/Monotonicity.lean
+++ b/Manual/Meta/Monotonicity.lean
@@ -4,38 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Joachim Breitner
 -/
 
-import Lean.Elab.Command
-import Lean.Elab.InfoTree
-
 import Verso
-import Verso.Doc.ArgParse
-import Verso.Doc.Elab.Monad
-import VersoManual
-import Verso.Code
-
-import SubVerso.Highlighting
-import SubVerso.Examples
 
 import Manual.Meta.Attribute
 import Manual.Meta.Basic
-import Manual.Meta.Bibliography
-import Manual.Meta.CustomStyle
-import Manual.Meta.Example
-import Manual.Meta.Figure
 import Manual.Meta.Lean
-import Manual.Meta.Lean.IO
-import Manual.Meta.Marginalia
-import Manual.Meta.ParserAlias
-import Manual.Meta.Syntax
 import Manual.Meta.Table
-import Manual.Meta.Tactics
-import Manual.Meta.SpliceContents
 
 open Lean Meta Elab
-open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
+open Verso Doc Elab
 open SubVerso.Highlighting Highlighted
 
-open Lean.Elab.Tactic.GuardMsgs
 
 namespace Manual
 

From 56b0219896008de8a350b4ff6d86681e3ddb3e9a Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 17 Jan 2025 17:03:22 +0100
Subject: [PATCH 14/27] Try to use a table (need help with the error)

---
 Manual/Meta/Monotonicity.lean | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
index 0b75c28..cb933e7 100644
--- a/Manual/Meta/Monotonicity.lean
+++ b/Manual/Meta/Monotonicity.lean
@@ -12,19 +12,32 @@ import Manual.Meta.Lean
 import Manual.Meta.Table
 
 open Lean Meta Elab
-open Verso Doc Elab
+open Verso Doc Elab Manual
 open SubVerso.Highlighting Highlighted
 
 
 namespace Manual
 
+def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : TermElabM Term := do
+  if h : rows.size = 0 then
+    throwError "Expected at least one row"
+  else
+    let columns := rows[0].size
+    if columns = 0 then
+      throwError "Expected at least one column"
+    if rows.any (·.size != columns) then
+      throwError s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}"
+
+    let blocks : Array (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.mk)
+    ``(Block.other (Block.table $(quote columns) $(quote header) $(quote name)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])
+
 @[block_role_expander monotonicityLemmas]
 def monotonicityLemmas : BlockRoleExpander
   | #[], #[] => do
     let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values
     let names := names.qsort (toString · < toString ·)
 
-    let itemStx : TSyntaxArray `term ← names.mapM fun name => do
+    let rows : Array (Array Syntax) ← names.mapM fun name => do
       -- Extract the target pattern
       let ci ← getConstInfo name
       let targetStx : TSyntax `term ←
@@ -42,10 +55,10 @@ def monotonicityLemmas : BlockRoleExpander
 
       let hl : Highlighted ← constTok name name.toString
       let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)])
-      `(Verso.Doc.Block.para #[$nameStx, Inline.text ": applies to ", $targetStx])
+      pure #[nameStx, targetStx]
 
-    let theList ← `(Verso.Doc.Block.ul #[$[⟨#[$itemStx]⟩],*])
-    return #[theList]
+    let tableStx ← mkTable rows "foo" "bar"
+    return #[tableStx]
   | _, _ => throwError "Unexpected arguments"
 
 -- #eval do

From 007582034f9fe2e1d97bce818584c9d7c92be577 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 17 Jan 2025 17:03:24 +0100
Subject: [PATCH 15/27] Revert "Try to use a table (need help with the error)"

This reverts commit 56b0219896008de8a350b4ff6d86681e3ddb3e9a.
---
 Manual/Meta/Monotonicity.lean | 23 +++++------------------
 1 file changed, 5 insertions(+), 18 deletions(-)

diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
index cb933e7..0b75c28 100644
--- a/Manual/Meta/Monotonicity.lean
+++ b/Manual/Meta/Monotonicity.lean
@@ -12,32 +12,19 @@ import Manual.Meta.Lean
 import Manual.Meta.Table
 
 open Lean Meta Elab
-open Verso Doc Elab Manual
+open Verso Doc Elab
 open SubVerso.Highlighting Highlighted
 
 
 namespace Manual
 
-def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : TermElabM Term := do
-  if h : rows.size = 0 then
-    throwError "Expected at least one row"
-  else
-    let columns := rows[0].size
-    if columns = 0 then
-      throwError "Expected at least one column"
-    if rows.any (·.size != columns) then
-      throwError s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}"
-
-    let blocks : Array (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.mk)
-    ``(Block.other (Block.table $(quote columns) $(quote header) $(quote name)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])
-
 @[block_role_expander monotonicityLemmas]
 def monotonicityLemmas : BlockRoleExpander
   | #[], #[] => do
     let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values
     let names := names.qsort (toString · < toString ·)
 
-    let rows : Array (Array Syntax) ← names.mapM fun name => do
+    let itemStx : TSyntaxArray `term ← names.mapM fun name => do
       -- Extract the target pattern
       let ci ← getConstInfo name
       let targetStx : TSyntax `term ←
@@ -55,10 +42,10 @@ def monotonicityLemmas : BlockRoleExpander
 
       let hl : Highlighted ← constTok name name.toString
       let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)])
-      pure #[nameStx, targetStx]
+      `(Verso.Doc.Block.para #[$nameStx, Inline.text ": applies to ", $targetStx])
 
-    let tableStx ← mkTable rows "foo" "bar"
-    return #[tableStx]
+    let theList ← `(Verso.Doc.Block.ul #[$[⟨#[$itemStx]⟩],*])
+    return #[theList]
   | _, _ => throwError "Unexpected arguments"
 
 -- #eval do

From ea47ac54efd767336f10af184129c49e3749df33 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 09:20:42 +0100
Subject: [PATCH 16/27] Reapply "Try to use a table (need help with the error)"

This reverts commit 007582034f9fe2e1d97bce818584c9d7c92be577.
---
 Manual/Meta/Monotonicity.lean | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
index 0b75c28..cb933e7 100644
--- a/Manual/Meta/Monotonicity.lean
+++ b/Manual/Meta/Monotonicity.lean
@@ -12,19 +12,32 @@ import Manual.Meta.Lean
 import Manual.Meta.Table
 
 open Lean Meta Elab
-open Verso Doc Elab
+open Verso Doc Elab Manual
 open SubVerso.Highlighting Highlighted
 
 
 namespace Manual
 
+def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : TermElabM Term := do
+  if h : rows.size = 0 then
+    throwError "Expected at least one row"
+  else
+    let columns := rows[0].size
+    if columns = 0 then
+      throwError "Expected at least one column"
+    if rows.any (·.size != columns) then
+      throwError s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}"
+
+    let blocks : Array (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.mk)
+    ``(Block.other (Block.table $(quote columns) $(quote header) $(quote name)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])
+
 @[block_role_expander monotonicityLemmas]
 def monotonicityLemmas : BlockRoleExpander
   | #[], #[] => do
     let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values
     let names := names.qsort (toString · < toString ·)
 
-    let itemStx : TSyntaxArray `term ← names.mapM fun name => do
+    let rows : Array (Array Syntax) ← names.mapM fun name => do
       -- Extract the target pattern
       let ci ← getConstInfo name
       let targetStx : TSyntax `term ←
@@ -42,10 +55,10 @@ def monotonicityLemmas : BlockRoleExpander
 
       let hl : Highlighted ← constTok name name.toString
       let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)])
-      `(Verso.Doc.Block.para #[$nameStx, Inline.text ": applies to ", $targetStx])
+      pure #[nameStx, targetStx]
 
-    let theList ← `(Verso.Doc.Block.ul #[$[⟨#[$itemStx]⟩],*])
-    return #[theList]
+    let tableStx ← mkTable rows "foo" "bar"
+    return #[tableStx]
   | _, _ => throwError "Unexpected arguments"
 
 -- #eval do

From f7f8c4260c57e4d3f0fa8f34e019ab80544bd0b5 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 09:50:55 +0100
Subject: [PATCH 17/27] Get table to work

---
 Manual/Meta/Monotonicity.lean | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
index cb933e7..366731f 100644
--- a/Manual/Meta/Monotonicity.lean
+++ b/Manual/Meta/Monotonicity.lean
@@ -18,7 +18,7 @@ open SubVerso.Highlighting Highlighted
 
 namespace Manual
 
-def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : TermElabM Term := do
+def mkInlineTabe (rows : Array (Array Term)) : TermElabM Term := do
   if h : rows.size = 0 then
     throwError "Expected at least one row"
   else
@@ -28,8 +28,10 @@ def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : Te
     if rows.any (·.size != columns) then
       throwError s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}"
 
-    let blocks : Array (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.mk)
-    ``(Block.other (Block.table $(quote columns) $(quote header) $(quote name)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])
+    -- let blocks : Array (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.ofElems)
+    let blocks : Array Term := rows.flatten
+    ``(Block.other (Block.table $(quote columns) False Option.none)
+        #[Block.ul #[$[Verso.Doc.ListItem.mk #[Block.para #[$blocks]]],*]])
 
 @[block_role_expander monotonicityLemmas]
 def monotonicityLemmas : BlockRoleExpander
@@ -37,7 +39,7 @@ def monotonicityLemmas : BlockRoleExpander
     let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values
     let names := names.qsort (toString · < toString ·)
 
-    let rows : Array (Array Syntax) ← names.mapM fun name => do
+    let rows : Array (Array Term) ← names.mapM fun name => do
       -- Extract the target pattern
       let ci ← getConstInfo name
       let targetStx : TSyntax `term ←
@@ -54,10 +56,11 @@ def monotonicityLemmas : BlockRoleExpander
             `(Inline.code $(quote str))
 
       let hl : Highlighted ← constTok name name.toString
-      let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)])
+      let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)}
+        #[Inline.code $(quote name.getString!)])
       pure #[nameStx, targetStx]
 
-    let tableStx ← mkTable rows "foo" "bar"
+    let tableStx ← mkInlineTabe rows
     return #[tableStx]
   | _, _ => throwError "Unexpected arguments"
 

From e16ca45a99bdd29ef103234ba4bebb40ea26ff1f Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 10:57:45 +0100
Subject: [PATCH 18/27] More on the table

---
 .../RecursiveDefs/PartialFixpoint.lean        | 19 +----
 Manual/Meta/Monotonicity.lean                 | 73 +++++++++++++++----
 2 files changed, 62 insertions(+), 30 deletions(-)

diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
index 6f030a2..ad69aad 100644
--- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean
@@ -327,23 +327,12 @@ The tactic solves goals of the form `monotone (fun x => …)` using the followin
 * Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on `x`.
 * Applying lemmas annotated with {attr}`partial_fixpoint_monotone`
 
-::::TODO
+{TODO}[I wonder if this needs to be collapsible. I at some point I had it in an example, but it's not really an example. Should be this collapsible? Is there a better way than to use example?]
 
-What I’d like to see here is
+{TODO}[This table probably needs some styling?]
 
-* {name}`Lean.Order.monotone_array_allM`: applies to `List.mapM ⬝ _`
-
-where I use `·` and `_` to distinguish the monotone arguments from others.
-
-::::
-
-:::example "List of Monotonicity Lemmas"
-
-{TODO}[Not really an example, but probably better to have this collapsible?]
-
-The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function:
+{TODO}[How can we I pretty-print these pattern expressions so that hovers work?]
 
+The following monotonicity lemmas are registered, and should allow recursive calls under the given higher-order functions in the arguments indicated by `.` (but not the other arguments, shown as `_`).
 
 {monotonicityLemmas}
-
-:::
diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
index 366731f..f114b07 100644
--- a/Manual/Meta/Monotonicity.lean
+++ b/Manual/Meta/Monotonicity.lean
@@ -18,7 +18,11 @@ open SubVerso.Highlighting Highlighted
 
 namespace Manual
 
-def mkInlineTabe (rows : Array (Array Term)) : TermElabM Term := do
+/--
+A table for monotonicity lemmas. Likely some of this logic can be extracted to a helper
+in `Manual/Meta/Table.lean`.
+-/
+private def mkInlineTabe (rows : Array (Array Term)) : TermElabM Term := do
   if h : rows.size = 0 then
     throwError "Expected at least one row"
   else
@@ -28,11 +32,34 @@ def mkInlineTabe (rows : Array (Array Term)) : TermElabM Term := do
     if rows.any (·.size != columns) then
       throwError s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}"
 
-    -- let blocks : Array (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.ofElems)
-    let blocks : Array Term := rows.flatten
-    ``(Block.other (Block.table $(quote columns) False Option.none)
+    let blocks : Array Term :=
+      #[ ← ``(Inline.text "Theorem"), ← ``(Inline.text "Pattern") ] ++
+      rows.flatten
+    ``(Block.other (Block.table $(quote columns) (header := true) Option.none)
         #[Block.ul #[$[Verso.Doc.ListItem.mk #[Block.para #[$blocks]]],*]])
 
+
+section delabhelpers
+
+/-!
+To format the monotonicy lemma patterns, I’d like to clearly mark the monotone arguments from
+the other arguments. So I define two gadgets with custom delaborators.
+-/
+
+def monoArg := @id
+def otherArg := @id
+
+open PrettyPrinter.Delaborator
+
+@[app_delab monoArg] def delabMonoArg : Delab :=
+  PrettyPrinter.Delaborator.withOverApp 2 `(·)
+@[app_delab otherArg] def delabOtherArg : Delab :=
+  PrettyPrinter.Delaborator.withOverApp 2 `(_)
+
+end delabhelpers
+
+
+
 @[block_role_expander monotonicityLemmas]
 def monotonicityLemmas : BlockRoleExpander
   | #[], #[] => do
@@ -42,23 +69,39 @@ def monotonicityLemmas : BlockRoleExpander
     let rows : Array (Array Term) ← names.mapM fun name => do
       -- Extract the target pattern
       let ci ← getConstInfo name
-      let targetStx : TSyntax `term ←
+
+      -- Omit the `Lean.Order` namespace, if present, to keep the table concise
+      let nameStr := (name.replacePrefix `Lean.Order .anonymous).getString!
+      let hl : Highlighted ← constTok name nameStr
+      let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)}
+        #[Inline.code $(quote nameStr)])
+
+      let patternStx : TSyntax `term ←
         forallTelescope ci.type fun _ concl => do
           unless concl.isAppOfArity ``Lean.Order.monotone 5 do
-            throwError "Unexpecte conclusion of {name}"
+            throwError "Unexpected conclusion of {name}"
           let f := concl.appArg!
           unless f.isLambda do
-            throwError "Unexpecte conclusion of {name}"
-          lambdaBoundedTelescope f 1 fun _ call => do
-            let stx ← Lean.PrettyPrinter.delab call
-            let format := Syntax.prettyPrint stx
-            let str := format.pretty'
+            throwError "Unexpected conclusion of {name}"
+          lambdaBoundedTelescope f 1 fun x call => do
+            -- Monotone arguments are the free variables applied to `x`,
+            -- Other arguments the other
+            -- This is an ad-hoc transformation and may fail in cases more complex
+            -- than we need right now (e.g. binders in the goal).
+            let call' ← Meta.transform call (pre := fun e => do
+              if e.isApp && e.appFn!.isFVar && e.appArg! == x[0]! then
+                .done <$> mkAppM ``monoArg #[e]
+              else if e.isFVar then
+                .done <$> mkAppM ``otherArg #[e]
+              else
+                pure .continue)
+
+            let stx ← Lean.PrettyPrinter.delab call'
+            let fmt ← Lean.PrettyPrinter.formatTerm stx
+            let str : String := fmt.pretty
             `(Inline.code $(quote str))
 
-      let hl : Highlighted ← constTok name name.toString
-      let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)}
-        #[Inline.code $(quote name.getString!)])
-      pure #[nameStx, targetStx]
+      pure #[nameStx, patternStx]
 
     let tableStx ← mkInlineTabe rows
     return #[tableStx]

From 7c36218e90e2f95876c1bc09a820fe2f534056ee Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 11:43:32 +0100
Subject: [PATCH 19/27] Use {name} not {inst}

---
 Manual/RecursiveDefs/PartialFixpoint.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean
index b529dfe..6a31363 100644
--- a/Manual/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/RecursiveDefs/PartialFixpoint.lean
@@ -22,13 +22,13 @@ tag := "partial-fixpoint"
 %%%
 
 A function definition can be understood as a request to Lean to construct a function of the given type that satisfies the given equation.
-One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {tech}[well-founded recursion] is to guarantee the existence and uniqueness the constructed functions.
+One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {ref "well-founded-recursion"}[well-founded recursion] is to guarantee the existence and uniqueness the constructed functions.
 
 In some cases, the equation may not uniquely determine the function's (extensional) behavior, because it
 does not terminate for all arguments in the above sense, but there still exist functions for which the defining equation holds.
 In these cases, a definition by {deftech}_partial fixpoint_ may be possible.
 
-Even in cases where the defining equation fully describes the function's behavior and a termination proof using {tech}[well-founded recursion] would be possible it may simply be more convenient to define the function using partial fixpoint, to avoid a possible tedious termination proof.
+Even in cases where the defining equation fully describes the function's behavior and a termination proof using {ref "well-founded-recursion"}[well-founded recursion] would be possible it may simply be more convenient to define the function using partial fixpoint, to avoid a possible tedious termination proof.
 
 Definition by partial fixpoint is only used when explicitly requested by the user, by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`.
 
@@ -88,7 +88,7 @@ partial_fixpoint
 ```
 
 More useful function definitions tend to have some branching.
-The following example can also be constructed using well-founded recursion with a termination proof, but may be more convenient to define using  {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`.
+The following example could also be constructed using well-founded recursion with a termination proof, but may be more convenient to define using  {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`, where no termination proof is needed.
 
 ```lean (keep := false)
 def Array.find (xs : Array α) (p : α → Bool) (i : Nat := 0) : Option α :=
@@ -308,7 +308,7 @@ variable (β : α → Sort v) [∀ x, CCPO (β x)]
 variable (w : α)
 ```
 
-* If the function's result type has a dedicated instance, like {name}`Option` has with {inst}`CCPO (Option α)`, this is used together with the instance for the function type, {inst}`CCPO (∀ x, β x)`, to construct an instance for the whole function's type.
+* If the function's result type has a dedicated instance, like {name}`Option` has with {name}`instCCPOOption`, this is used together with the instance for the function type, {name}`instCCPOPi`, to construct an instance for the whole function's type.
 
 * Else, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {inst}`CCPO (FlatOrder w)` is used, `w` is a least element and all other elements are incomparable.
 

From 370914260168cb68f51429981446709bc3d88cd4 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 12:06:39 +0100
Subject: [PATCH 20/27] cargo-cult local syntax tricks

---
 Manual/RecursiveDefs/PartialFixpoint.lean | 25 +++++++++++++++++------
 1 file changed, 19 insertions(+), 6 deletions(-)

diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean
index 6a31363..c33210c 100644
--- a/Manual/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/RecursiveDefs/PartialFixpoint.lean
@@ -310,7 +310,7 @@ variable (w : α)
 
 * If the function's result type has a dedicated instance, like {name}`Option` has with {name}`instCCPOOption`, this is used together with the instance for the function type, {name}`instCCPOPi`, to construct an instance for the whole function's type.
 
-* Else, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {inst}`CCPO (FlatOrder w)` is used, `w` is a least element and all other elements are incomparable.
+* Else, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {name}`FlatOrder.instCCPO` for the wrapper type {lean}`FlatOrder w` is used. In this order, {lean}`w` is a least element and all other elements are incomparable.
 
 ```lean (show := false)
 end
@@ -318,18 +318,31 @@ end
 
 Next, the recursive calls in the right-hand side of the function definitions are abstracted; this turns into the argument `f` of {name}`fix`. The monotonicity requirement is solved by the {tactic}`monotonicity` tactic, which applies compositional monotonicity lemmas in a syntax-driven way
 
-The tactic solves goals of the form `monotone (fun x => …)` using the following steps:
+```lean (show := false)
+section
+set_option linter.unusedVariables false
+variable {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] (more : (x : α) → β) (x : α)
+
+local macro "…" x:term:arg "…" : term => `(more $x)
+```
+
+The tactic solves goals of the form {lean}`monotone (fun x => … x …)` using the following steps:
 
-* Applying {name}`monotone_const` when there is no dependency on `x` left.
+* Applying {name}`monotone_const` when there is no dependency on {lean}`x` left.
 * Splitting on {keywordOf Lean.Parser.Term.match}`match` expressions.
 * Splitting on {keywordOf termIfThenElse}`if` expressions.
-* Moving {keywordOf Lean.Parser.Term.let}`let` expression to the context, if the value and type do not depend on `x`.
-* Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on `x`.
+* Moving {keywordOf Lean.Parser.Term.let}`let` expression to the context, if the value and type do not depend on {lean}`x`.
+* Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on {lean}`x`.
 * Applying lemmas annotated with {attr}`partial_fixpoint_monotone`
 
+```lean (show := false)
+end
+```
+
+
 {TODO}[I wonder if this needs to be collapsible. I at some point I had it in an example, but it's not really an example. Should be this collapsible? Is there a better way than to use example?]
 
-{TODO}[This table probably needs some styling?]
+{TODO}[This table probably needs some styling? Less vertical space maybe?]
 
 {TODO}[How can we I pretty-print these pattern expressions so that hovers work?]
 

From 37020b8fa50cbb4625bcca08621a4755ee3e3806 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 12:15:51 +0100
Subject: [PATCH 21/27] Copy editing

---
 Manual/RecursiveDefs/PartialFixpoint.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean
index c33210c..929633c 100644
--- a/Manual/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/RecursiveDefs/PartialFixpoint.lean
@@ -140,7 +140,7 @@ In particular, using {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation] should
 
 :::example "Monadic functions"
 
-The following function implements the Ackermann function in the {name}`Option` monad, and is accepted without a (explicit or implicit) termination proof:
+The following function implements the Ackermann function in the {name}`Option` monad, and is accepted without an (explicit or implicit) termination proof:
 
 ```lean (keep := false)
 def ack : (n m : Nat) → Option Nat
@@ -150,7 +150,7 @@ def ack : (n m : Nat) → Option Nat
 partial_fixpoint
 ```
 
-Recursion can also happen within higher-order library functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]:
+Recursive calls may also occur Escurisve within higher-order functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]:
 
 ```lean (keep := false)
 structure Tree where cs : List Tree
@@ -256,7 +256,8 @@ We can use this theorem to prove that the resulting number is a valid index in t
 ```lean
 theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) :
     xs.findIndex p = some i → xs[i]?.any p := by
-  apply List.findIndex.partial_correctness (motive := fun xs p i => xs[i]?.any p)
+  apply List.findIndex.partial_correctness
+          (motive := fun xs p i => xs[i]?.any p)
   intro findIndex ih xs p r hsome
   split at hsome
   next => contradiction

From 7c0d7ad1e63e1a336428e158075c521df6c2abde Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 12:22:21 +0100
Subject: [PATCH 22/27] A (not very interesting) mutual recursion section

---
 Manual/RecursiveDefs/PartialFixpoint.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean
index 929633c..8e45a0f 100644
--- a/Manual/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/RecursiveDefs/PartialFixpoint.lean
@@ -275,6 +275,17 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) :
 
 :::
 
+# Mutual Well-Founded Recursion
+%%%
+tag := "mutual-well-founded-recursion"
+%%%
+
+Lean supports the definition of {tech}[mutually recursive] functions using {tech}[partial fixpoint].
+Mutual recursion may be introduced using a {tech}[mutual block], but it also results from {keywordOf Lean.Parser.Term.letrec}`let rec` expressions and {keywordOf Lean.Parser.Command.declaration}`where` blocks.
+The rules for mutual well-founded recursion are applied to a group of actually mutually recursive, lifted definitions, that results from the {ref "mutual-syntax"}[elaboration steps] for mutual groups.
+
+If all functions in the mutual group have the {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` clause, then this strategy is used.
+
 # Theory and Construction
 %%%
 tag := "partial-fixpoint-theory"

From 95a0625dc667661dd5eebcd10fb4adfa48552c16 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 12:23:29 +0100
Subject: [PATCH 23/27] Typo

---
 Manual/RecursiveDefs/PartialFixpoint.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean
index 8e45a0f..a3a3a49 100644
--- a/Manual/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/RecursiveDefs/PartialFixpoint.lean
@@ -150,7 +150,7 @@ def ack : (n m : Nat) → Option Nat
 partial_fixpoint
 ```
 
-Recursive calls may also occur Escurisve within higher-order functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]:
+Recursive calls may also occur within higher-order functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]:
 
 ```lean (keep := false)
 structure Tree where cs : List Tree

From 39f81f1a6e36e68ea6d58102fdefc36eef38e097 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 14:28:16 +0100
Subject: [PATCH 24/27] Avoid duplicate anchor

---
 Manual/RecursiveDefs/PartialFixpoint.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean
index a3a3a49..59d9169 100644
--- a/Manual/RecursiveDefs/PartialFixpoint.lean
+++ b/Manual/RecursiveDefs/PartialFixpoint.lean
@@ -277,7 +277,7 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) :
 
 # Mutual Well-Founded Recursion
 %%%
-tag := "mutual-well-founded-recursion"
+tag := "mutual-partial-fixpoint"
 %%%
 
 Lean supports the definition of {tech}[mutually recursive] functions using {tech}[partial fixpoint].

From 8478f381f2b164ffade718861a56b3c2bcfbca83 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2025 22:22:34 +0100
Subject: [PATCH 25/27] Use ppExpr

---
 Manual/Meta/Monotonicity.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
index f114b07..547e01f 100644
--- a/Manual/Meta/Monotonicity.lean
+++ b/Manual/Meta/Monotonicity.lean
@@ -96,10 +96,8 @@ def monotonicityLemmas : BlockRoleExpander
               else
                 pure .continue)
 
-            let stx ← Lean.PrettyPrinter.delab call'
-            let fmt ← Lean.PrettyPrinter.formatTerm stx
-            let str : String := fmt.pretty
-            `(Inline.code $(quote str))
+            let fmt ← ppExpr call'
+            `(Inline.code $(quote fmt.pretty))
 
       pure #[nameStx, patternStx]
 

From 5b8409aa105974d3bd2b8d834ab50f6617ec1e98 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 22 Jan 2025 14:19:52 +0100
Subject: [PATCH 26/27] Bump to nightly

---
 lake-manifest.json | 2 +-
 lean-toolchain     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 34a71e2..2ff79ee 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "844b9a53cf7acd71e0e81a3a56608bb28215646d",
+   "rev": "73ee3629d01f3255b23645f56d8e587e1337a01f",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 12fc5b0..2a88805 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4-pr-releases:pr-release-6355
+leanprover/lean4-nightly:nightly-2025-01-22

From 13f0ba9fde5fbe8675483c94404a76b6eb487502 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 22 Jan 2025 14:40:18 +0100
Subject: [PATCH 27/27] Make build work with nightly

---
 Manual/BasicTypes/String/FFI.lean | 2 +-
 Manual/RecursiveDefs/WF.lean      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Manual/BasicTypes/String/FFI.lean b/Manual/BasicTypes/String/FFI.lean
index 171c1d4..7e9165b 100644
--- a/Manual/BasicTypes/String/FFI.lean
+++ b/Manual/BasicTypes/String/FFI.lean
@@ -20,7 +20,7 @@ tag := "string-ffi"
 %%%
 
 
-{docstring String.csize}
+{docstring Char.utf8Size}
 
 :::ffi "lean_string_object" kind := type
 ```
diff --git a/Manual/RecursiveDefs/WF.lean b/Manual/RecursiveDefs/WF.lean
index e05127c..f81c5bb 100644
--- a/Manual/RecursiveDefs/WF.lean
+++ b/Manual/RecursiveDefs/WF.lean
@@ -412,7 +412,7 @@ In particular, it tries the following tactics and theorems:
 
 * {tactic}`simp_arith`
 * {tactic}`assumption`
-* theorems {name}`Nat.sub_succ_lt_self`, {name}`Nat.pred_lt'`, {name}`Nat.pred_lt`, which handle common arithmetic goals
+* theorems {name}`Nat.sub_succ_lt_self`, {name}`Nat.pred_lt_of_lt`, {name}`Nat.pred_lt`, which handle common arithmetic goals
 * {tactic}`omega`
 * {tactic}`array_get_dec` and {tactic}`array_mem_dec`, which prove that the size of array elements is less than the size of the array
 * {tactic}`sizeOf_list_dec` that the size of list elements is less than the size of the list