From 4fbdaeaa385e66c39e917cd3cc48da2a2bd82ad2 Mon Sep 17 00:00:00 2001 From: ia0 Date: Wed, 15 Jul 2026 14:56:23 +0200 Subject: [PATCH 1/2] doc: fix typos in Defs and RecursiveDefs --- Manual/Defs.lean | 4 ++-- Manual/RecursiveDefs/CoinductivePredicates.lean | 2 +- Manual/RecursiveDefs/PartialFixpoint.lean | 6 +++--- Manual/RecursiveDefs/Structural/RecursorExample.lean | 2 +- Manual/RecursiveDefs/WF.lean | 2 +- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Manual/Defs.lean b/Manual/Defs.lean index d6b99f484..2ffa39d60 100644 --- a/Manual/Defs.lean +++ b/Manual/Defs.lean @@ -253,7 +253,7 @@ tag := "automatic-implicit-parameters" %%% -By default, otherwise-unbound names that occur in signatures are converted into implicit parameters when possible +By default, otherwise-unbound names that occur in signatures are converted into implicit parameters when possible. These parameters are called {deftech}_automatic implicit parameters_. This is possible when they are not in the function position of an application and when there is sufficient information available in the signature to infer their type and any ordering constraints on them. This process is iterated: if the inferred type for the freshly-inserted implicit parameter has dependencies that are not uniquely determined, then these dependencies are replaced with further implicit parameters. @@ -392,7 +392,7 @@ AtLeast.add {n✝ : Nat} {i : Fin n✝} (x y : AtLeast i) : AtLeast i ::::: Automatic implicit parameter insertion takes place after the insertion of parameters due to {tech}[section variables]. -Parameters that correspond to section variables have the same name as the corresponding variable, even when they do not correspond to a name written directly in the signature, and disabling automatic implicit parameters has no effect the parameters that correspond to section variables. +Parameters that correspond to section variables have the same name as the corresponding variable, even when they do not correspond to a name written directly in the signature, and disabling automatic implicit parameters has no effect on the parameters that correspond to section variables. However, when automatic implicit parameters are enabled, section variable declarations that contain otherwise-unbound variables receive additional section variables that follow the same rules as those for implicit parameters. Automatic implicit parameters insertion is controlled by two options. diff --git a/Manual/RecursiveDefs/CoinductivePredicates.lean b/Manual/RecursiveDefs/CoinductivePredicates.lean index 5f68dcbd8..64d0c8c66 100644 --- a/Manual/RecursiveDefs/CoinductivePredicates.lean +++ b/Manual/RecursiveDefs/CoinductivePredicates.lean @@ -73,7 +73,7 @@ variable {R : α → α → Prop} (a : α) {pred : α → Prop} The coinductive reasoning principle takes a predicate {lean}`pred`. To prove that {lean}`a` is the start of an infinite {lean}`R`-sequence, it suffices to show that {lean}`R` relates each element that satisfies {lean}`pred` to some other such element. -In other words, it that the presence of an infinite sequence can be demonstrated by providing one: +In other words, that the presence of an infinite sequence can be demonstrated by providing one: ```signature InfSeq.coinduct (R : α → α → Prop) (pred : α → Prop) : (∀ (a : α), pred a → ∃ y, R a y ∧ pred y) → diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index bfa464837..6bbdde3cb 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -40,12 +40,12 @@ As with the other strategies for defining recursive functions, compiled code use The term {tech}_partial fixpoint_ is specific to Lean. Functions declared {keywordOf Lean.Parser.Command.declaration}`partial` do not require termination proofs, so long as the type of their return values is inhabited, but they are completely opaque from the perspective of Lean's logic. Partial fixpoints, on the other hand, can be rewritten using their defining equations while writing proofs. -Logically speaking, partial fixpoints are total functions that don't reduce {tech (key := "definitional equality")}[definitionally] when applied, but for which equational rewrite rule are provided. +Logically speaking, partial fixpoints are total functions that don't reduce {tech (key := "definitional equality")}[definitionally] when applied, but for which equational rewrite rules are provided. They are _partial_ in the sense that the defining equation does not necessarily specify a value for all possible arguments. While partial fixpoints do allow functions to be defined that cannot be expressed using structural or well-founded recursion, the technique is also useful in other cases. -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 as a partial fixpoint to avoid a having to write a 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 as a partial fixpoint to avoid having to write a termination proof. Defining recursive functions as partial fixpoints only occurs when explicitly requested by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. @@ -191,7 +191,7 @@ tag := "partial-fixpoint-monadic" Defining a function as a partial fixpoint is more powerful if the function's return type is a monad that is an instance of {name}`Lean.Order.MonoBind`, such as {name}`Option`. -In this case, recursive call are not restricted to tail-positions, but may also occur inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`. +In this case, recursive calls are not restricted to tail-positions, but may also occur inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`. The set of higher-order functions for which this works is {ref "partial-fixpoint-theory"}[extensible], 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 that does not open the abstraction of the monad (e.g. by matching on the {name}`Option` value), is accepted. diff --git a/Manual/RecursiveDefs/Structural/RecursorExample.lean b/Manual/RecursiveDefs/Structural/RecursorExample.lean index cc9f1cc8b..768e24938 100644 --- a/Manual/RecursiveDefs/Structural/RecursorExample.lean +++ b/Manual/RecursiveDefs/Structural/RecursorExample.lean @@ -76,7 +76,7 @@ noncomputable def half'' (n : Nat) : Nat := | 0, _ | 1, _ => 0 | _ + 2, ⟨_, ⟨h, _⟩⟩ => h + 1 ``` -The function is marked {keywordOf Lean.Parser.Command.declaration}`noncomputable` because the compiler doesn't support generating code for course-of-values recursion, which is intended for reasoning rather that efficient code. +The function is marked {keywordOf Lean.Parser.Command.declaration}`noncomputable` because the compiler doesn't support generating code for course-of-values recursion, which is intended for reasoning rather than efficient code. The kernel can still be used to test the function, however: ```lean (name := halfTest2) #reduce [0,1,2,3,4,5,6,7,8].map half'' diff --git a/Manual/RecursiveDefs/WF.lean b/Manual/RecursiveDefs/WF.lean index 2ca0fbb81..43b354bbe 100644 --- a/Manual/RecursiveDefs/WF.lean +++ b/Manual/RecursiveDefs/WF.lean @@ -798,7 +798,7 @@ This is typically done in two steps: This theorem uses the {name}`binderNameHint` gadget to preserve a user-chosen binder name, should {lean}`f` be a lambda expression. -By separating the introduction of {name}`List.attach` from the propagation of the introduced assumption, the desired the {lean}`x ∈ xs` assumption is made available to {lean}`f` even in chains such as `(xs.reverse.filter p).map f`. +By separating the introduction of {name}`List.attach` from the propagation of the introduced assumption, the desired {lean}`x ∈ xs` assumption is made available to {lean}`f` even in chains such as `(xs.reverse.filter p).map f`. ::: From f379914249f34e794c544ad6376fb833980edd00 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 27 Jul 2026 14:01:24 +0200 Subject: [PATCH 2/2] Apply suggestion from @david-christiansen --- Manual/RecursiveDefs/CoinductivePredicates.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/RecursiveDefs/CoinductivePredicates.lean b/Manual/RecursiveDefs/CoinductivePredicates.lean index 64d0c8c66..70816e45f 100644 --- a/Manual/RecursiveDefs/CoinductivePredicates.lean +++ b/Manual/RecursiveDefs/CoinductivePredicates.lean @@ -73,7 +73,7 @@ variable {R : α → α → Prop} (a : α) {pred : α → Prop} The coinductive reasoning principle takes a predicate {lean}`pred`. To prove that {lean}`a` is the start of an infinite {lean}`R`-sequence, it suffices to show that {lean}`R` relates each element that satisfies {lean}`pred` to some other such element. -In other words, that the presence of an infinite sequence can be demonstrated by providing one: +In other words, the presence of an infinite sequence can be demonstrated by providing one: ```signature InfSeq.coinduct (R : α → α → Prop) (pred : α → Prop) : (∀ (a : α), pred a → ∃ y, R a y ∧ pred y) →