From c25da07f93a3d8200cbbc45184f2c35106698bfc Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 29 Dec 2025 03:43:39 -0800 Subject: [PATCH] doc: fix error explanation wording --- Manual/ErrorExplanations/InferDefTypeFailed.lean | 2 +- Manual/ErrorExplanations/InvalidField.lean | 2 +- Manual/ErrorExplanations/SynthInstanceFailed.lean | 2 +- Manual/Meta/ErrorExplanation/Header.lean | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Manual/ErrorExplanations/InferDefTypeFailed.lean b/Manual/ErrorExplanations/InferDefTypeFailed.lean index 842fe0b99..b6e8be5e8 100644 --- a/Manual/ErrorExplanations/InferDefTypeFailed.lean +++ b/Manual/ErrorExplanations/InferDefTypeFailed.lean @@ -33,7 +33,7 @@ ambiguities that may be contributing to this error. Note that when an explicit resulting type is provided—even if that type contains holes—Lean will not use information from the definition body to help infer the type of the definition or its parameters. Thus, adding an explicit resulting type may also necessitate adding type annotations to parameters -whose types were previously inferrable. Additionally, it is always necessary to provide an explicit +whose types were previously inferable. Additionally, it is always necessary to provide an explicit type in a `theorem` declaration: the `theorem` syntax requires a type annotation, and the elaborator will never attempt to use the theorem body to infer the proposition being proved. diff --git a/Manual/ErrorExplanations/InvalidField.lean b/Manual/ErrorExplanations/InvalidField.lean index 59ca75799..6707fbca6 100644 --- a/Manual/ErrorExplanations/InvalidField.lean +++ b/Manual/ErrorExplanations/InvalidField.lean @@ -78,7 +78,7 @@ def double_plus_one (x : Nat) := (x + x).succ ``` -The `Add` typeclass is sufficient for performing the addition `x + x`, but the `.succ` field notation +The `Add` type class is sufficient for performing the addition `x + x`, but the `.succ` field notation cannot operate without knowing more about the actual type from which `succ` is being projected. ::: diff --git a/Manual/ErrorExplanations/SynthInstanceFailed.lean b/Manual/ErrorExplanations/SynthInstanceFailed.lean index c95a8b07b..e4034b844 100644 --- a/Manual/ErrorExplanations/SynthInstanceFailed.lean +++ b/Manual/ErrorExplanations/SynthInstanceFailed.lean @@ -22,7 +22,7 @@ variable {t : Type} (x y : Int) {ref "type-classes"}[Type classes] are the mechanism that Lean and many other programming languages use to handle overloaded operations. The code that handles a particular -overloaded operation is an {tech}_instance_ of a typeclass; deciding which instance to use for a given +overloaded operation is an {tech}_instance_ of a type class; deciding which instance to use for a given overloaded operation is called _synthesizing_ an instance. As an example, when Lean encounters an expression {lean}`x + y` where {lean}`x` and {lean}`y` both diff --git a/Manual/Meta/ErrorExplanation/Header.lean b/Manual/Meta/ErrorExplanation/Header.lean index c9517d7ef..a20dd9a5f 100644 --- a/Manual/Meta/ErrorExplanation/Header.lean +++ b/Manual/Meta/ErrorExplanation/Header.lean @@ -116,7 +116,7 @@ def errorExplanationHeader : Verso.Doc.Elab.BlockCommandOf ErrorHeaderConfig | cfg, _contents => do match ← getErrorExplanation? cfg.name with | .none => - Lean.logWarning m!"The named error `{cfg.name}` is not not known by the Lean compiler" + Lean.logWarning m!"The named error `{cfg.name}` is not known by the Lean compiler" let metadata := ErrorExplanationExtendedMetadata.mk (ErrorExplanation.Metadata.mk "Summary unavailable" "Metadata unavailable" MessageSeverity.error Option.none) cfg.name ``(Doc.Block.other (Block.errorExplanationHeader $(quote metadata)) #[]) | .some explan =>