From 1e1ed16a05f8e784e34e7e58c35df9931b4cdcb3 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 1 Dec 2025 22:38:05 -0800 Subject: [PATCH] doc: correct typos in documentation and comments (#11465) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes various typos across the codebase in documentation and comments. - `infered` → `inferred` (ParserCompiler.lean) - `declartation` → `declaration` (Cleanup.lean) - `certian` → `certain` (CasesInfo.lean) - `wil` → `will` (Cache.lean) - `the the` → `the` (multiple files - PrefixTree.lean, Sum/Basic.lean, List/Nat/Perm.lean, Time.lean, Bounded.lean, Lake files) - `to to` → `to` (MutualInductive.lean, simp_bubblesort_256.lean) - Grammar improvements in Bounded.lean and Time.lean All changes are to comments and documentation only - no functional changes. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude --- src/Init/Data/List/Nat/Perm.lean | 4 ++-- src/Init/Data/Sum/Basic.lean | 2 +- src/Lean/Data/PrefixTree.lean | 2 +- src/Lean/Elab/MutualInductive.lean | 2 +- src/Lean/Meta/CasesInfo.lean | 2 +- src/Lean/Meta/Tactic/Cleanup.lean | 2 +- src/Lean/ParserCompiler.lean | 2 +- src/Std/Time.lean | 2 +- src/Std/Time/Internal/Bounded.lean | 4 ++-- src/lake/Lake/Build/Common.lean | 2 +- src/lake/Lake/CLI/Help.lean | 2 +- src/lake/Lake/Config/Cache.lean | 6 +++--- tests/bench/simp_bubblesort_256.lean | 2 +- 13 files changed, 17 insertions(+), 17 deletions(-) diff --git a/src/Init/Data/List/Nat/Perm.lean b/src/Init/Data/List/Nat/Perm.lean index 395f0f40be..5ef9790000 100644 --- a/src/Init/Data/List/Nat/Perm.lean +++ b/src/Init/Data/List/Nat/Perm.lean @@ -60,14 +60,14 @@ theorem set_set_perm {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : j namespace Perm -/-- Variant of `List.Perm.take` specifying the the permutation is constant after `i` elementwise. -/ +/-- Variant of `List.Perm.take` specifying that the permutation is constant after `i` elementwise. -/ theorem take_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, i ≤ j → l₁[j]? = l₂[j]?) : l₁.take i ~ l₂.take i := by refine h.take (Perm.of_eq ?_) ext1 j simpa using w (i + j) (by omega) -/-- Variant of `List.Perm.drop` specifying the the permutation is constant before `i` elementwise. -/ +/-- Variant of `List.Perm.drop` specifying that the permutation is constant before `i` elementwise. -/ theorem drop_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, j < i → l₁[j]? = l₂[j]?) : l₁.drop i ~ l₂.drop i := by refine h.drop (Perm.of_eq ?_) diff --git a/src/Init/Data/Sum/Basic.lean b/src/Init/Data/Sum/Basic.lean index 2ac59b995c..61bb9a4f80 100644 --- a/src/Init/Data/Sum/Basic.lean +++ b/src/Init/Data/Sum/Basic.lean @@ -13,7 +13,7 @@ public section /-! # Disjoint union of types -This file defines basic operations on the the sum type `α ⊕ β`. +This file defines basic operations on the sum type `α ⊕ β`. `α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*. diff --git a/src/Lean/Data/PrefixTree.lean b/src/Lean/Data/PrefixTree.lean index 12fa45a3e0..cd7f2a01b9 100644 --- a/src/Lean/Data/PrefixTree.lean +++ b/src/Lean/Data/PrefixTree.lean @@ -52,7 +52,7 @@ partial def find? (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) | some t => loop t ks loop t k -/-- Returns the the value of the longest key in `t` that is a prefix of `k`, if any. -/ +/-- Returns the value of the longest key in `t` that is a prefix of `k`, if any. -/ @[inline] partial def findLongestPrefix? (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) : Option β := let rec @[specialize] loop acc? diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 83740eb3d0..acffab1b27 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -1173,7 +1173,7 @@ private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) (is let throwErrorsAt (init cur : Syntax) (msg : MessageData) : TermElabM Unit := do logErrorAt init msg throwErrorAt cur msg - -- Maps names of inductive types to to `true` and those of constructors to `false`, along with syntax refs + -- Maps names of inductive types to `true` and those of constructors to `false`, along with syntax refs let mut uniqueNames : Std.HashMap Name (Bool × Syntax) := {} let declString := if isCoinductive then "coinductive predicate" else "inductive type" trace[Elab.inductive] "deckString: {declString}" diff --git a/src/Lean/Meta/CasesInfo.lean b/src/Lean/Meta/CasesInfo.lean index f447e64c92..9913b52672 100644 --- a/src/Lean/Meta/CasesInfo.lean +++ b/src/Lean/Meta/CasesInfo.lean @@ -26,7 +26,7 @@ It is used in particular by the code generator to replace calls to such function `cases` construct. The `getSparseCasesInfo?` function calculates the `CasesInfo` from the type of the declaration, and -makes certian assumptions about their shapes. If this is too fragile, the `sparseCasesOn` env +makes certain assumptions about their shapes. If this is too fragile, the `sparseCasesOn` env extension could carry more information from which the shape can be calculated.. -/ diff --git a/src/Lean/Meta/Tactic/Cleanup.lean b/src/Lean/Meta/Tactic/Cleanup.lean index 071ab24b71..36dabba101 100644 --- a/src/Lean/Meta/Tactic/Cleanup.lean +++ b/src/Lean/Meta/Tactic/Cleanup.lean @@ -72,7 +72,7 @@ where - It occurs in the target type, or - There is a relevant variable `y` that depends on `x`, or - If `indirectProps` is true, the type of `x` is a proposition and it depends on a relevant variable `y`. - - If `indirectProps` is true, `x` is a local declartation and its value mentions a relevant variable `y`. + - If `indirectProps` is true, `x` is a local declaration and its value mentions a relevant variable `y`. By default, `toPreserve := #[]` and `indirectProps := true`. These settings are used in the mathlib tactic `extract_goal` to give the user more control over which variables to include. diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index f3921fb3d5..360c598846 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -107,7 +107,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do name := c', levelParams := [] type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } - -- usually `meta` is infered during compilation for auxiliary definitions, but as + -- usually `meta` is inferred during compilation for auxiliary definitions, but as -- `ctx.combinatorAttr` may enforce correct use of the modifier, infer now. if isMarkedMeta (← getEnv) c then modifyEnv (markMeta · c') diff --git a/src/Std/Time.lean b/src/Std/Time.lean index fbfcaa8616..bd73a0c29f 100644 --- a/src/Std/Time.lean +++ b/src/Std/Time.lean @@ -171,7 +171,7 @@ The supported formats include: - `EEEE`: Displays the full day name (e.g., "Tuesday"). - `EEEEE`: Displays the narrow day name (e.g., "T" for Tuesday). - `e`: Represents the weekday as number or text. - - `e`, `ee`: Displays the the as a number, starting from 1 (Monday) to 7 (Sunday). + - `e`, `ee`: Displays the weekday as a number, starting from 1 (Monday) to 7 (Sunday). - `eee`, `eeee`, `eeeee`: Displays the weekday as text (same format as `E`). - `F`: Represents the week of the month that the first week starts on the first day of the month (e.g., "3"). - `a`: Represents the AM or PM designation of the day. diff --git a/src/Std/Time/Internal/Bounded.lean b/src/Std/Time/Internal/Bounded.lean index 00395c2d5f..faf8bd0300 100644 --- a/src/Std/Time/Internal/Bounded.lean +++ b/src/Std/Time/Internal/Bounded.lean @@ -61,7 +61,7 @@ instance : LawfulEqOrd (Bounded rel n m) where variable {rel a b} /-- -A `Bounded` integer that the relation used is the the less-equal relation so, it includes all +A `Bounded` integer where the relation used is the less-equal relation, so it includes all integers that `lo ≤ val ≤ hi`. -/ abbrev LE := @Bounded LE.le @@ -74,7 +74,7 @@ def cast {rel : Int → Int → Prop} {lo₁ lo₂ hi₁ hi₂ : Int} (h₁ : lo .mk b.val ⟨h₁ ▸ b.property.1, h₂ ▸ b.property.2⟩ /-- -A `Bounded` integer that the relation used is the the less-than relation so, it includes all +A `Bounded` integer where the relation used is the less-than relation, so it includes all integers that `lo < val < hi`. -/ abbrev LT := @Bounded LT.lt diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index 264291101a..915abd4ff5 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -499,7 +499,7 @@ public class ResolveOutputs (m : Type v → Type w) (α : Type v) where open ResolveOutputs in /-- -Retrieve artifacts from the Lake cache using the the outputs stored +Retrieve artifacts from the Lake cache using the outputs stored in either the saved trace file or in the cached input-to-content mapping. **For internal use only.** diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index db3446a4b9..bba4a18e84 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -406,7 +406,7 @@ Artifacts are uploaded to the artifact endpoint with a file name derived from their Lake content hash (and prefixed by the repository or scope). The mappings file is uploaded to the revision endpoint with a file name derived from the package's current Git revision (and prefixed by the -full scope). As such, the command will warn if the the work tree currently +full scope). As such, the command will warn if the work tree currently has changes." def helpScriptCli := diff --git a/src/lake/Lake/Config/Cache.lean b/src/lake/Lake/Config/Cache.lean index 8bf9b53824..2961889714 100644 --- a/src/lake/Lake/Config/Cache.lean +++ b/src/lake/Lake/Config/Cache.lean @@ -90,7 +90,7 @@ public partial def parse (inputName : String) (contents : String) : LoggerIO Cac /-- Loads a `CacheMap` from a JSON Lines file. -Errors if the the file is ill-formatted or the read fails for other reasons. +Errors if the file is ill-formatted or the read fails for other reasons. -/ public def load (file : FilePath) : LogIO CacheMap := do match (← IO.FS.Handle.mk file .read |>.toBaseIO) with @@ -255,7 +255,7 @@ public def getArtifactPaths @[inline] public def outputsDir (cache : Cache) : FilePath := cache.dir / "outputs" -/-- The file containing the outputs of the the given input for the package. -/ +/-- The file containing the outputs of the given input for the package. -/ @[inline] public def outputsFile (cache : Cache) (scope : String) (inputHash : Hash) : FilePath := cache.outputsDir / scope / s!"{inputHash}.json" @@ -359,7 +359,7 @@ namespace CacheService /-- Reconfigures the cache service to interpret scopes as repositories (or not if `false`). -For custom endpoints, if `true`, Lake wil augment the provided scope with +For custom endpoints, if `true`, Lake will augment the provided scope with toolchain and platform information in a manner similar to Reservoir. -/ @[inline] public def withRepoScope (service : CacheService) (repoScope := true) : CacheService := diff --git a/tests/bench/simp_bubblesort_256.lean b/tests/bench/simp_bubblesort_256.lean index 148f6b6226..f63c3f1776 100644 --- a/tests/bench/simp_bubblesort_256.lean +++ b/tests/bench/simp_bubblesort_256.lean @@ -6,7 +6,7 @@ This uses axiom to make it independent of specific optimization (e.g. for `Nat`). It generates a “list” of 128 `b`s followed by 128 `a` and uses -bubble-sort to to sort it and compares it against the expected output. +bubble-sort to sort it and compares it against the expected output. -/ inductive V where | a | b