style: fix spelling errors in Lean/ docstrings

src/Lean/Compiler/InlineAttrs.lean

@@ -40,7 +40,7 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do
     declName' == ``WellFounded.Nat.fix ||
     declName' == declName ++ `_unary -- Auxiliary declaration created by `WF` module
   if Option.isSome <| info.value.find? fun e => e.isConst && isRec e.constName! then
-    -- It contains a `brecOn` or `WellFounded.fix` application. So, it should be recursvie
+    -- It contains a `brecOn` or `WellFounded.fix` application. So, it should be recursive
     return false
   return true
 

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -287,7 +287,7 @@ abbrev ExtendM := ReaderT ExtendContext StateRefT ExtendState ScopeM
 Replace a free variable if necessary, that is:
 - It is in the list of candidates
 - We are currently within a join point (if we are within a function there
-  cannot be a need to replace them since we dont extend their context)
+  cannot be a need to replace them since we don't extend their context)
 - Said join point actually has a replacement parameter registered.
 otherwise just return `fvar`.
 -/

src/Lean/Compiler/LCNF/Specialize.lean

@@ -226,7 +226,7 @@ def shouldSpecialize (specEntry : SpecEntry) (args : Array Arg) : SpecializeM Bo
         If we have `f p` where `p` is a param it makes no sense to specialize as we will just
         close over `p` again and will have made no progress.
 
-        The reason for doing this only for declarations which have have already been specialised
+        The reason for doing this only for declarations which have already been specialised
         themselves is, that we *must* always specialize declarations that are marked with
         `@[specialize]`. This is because the specializer will not specialize their bodies because it
         waits for the bodies to be specialized at the call site. This is for example important in

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -92,7 +92,7 @@ def declIsNotUnsafe (declName : Name) : CoreM Bool := do
     return false
   else
     if info matches .opaqueInfo .. then
-      -- check if its a partial def
+      -- check if it's a partial def
       return env.find? (Compiler.mkUnsafeRecName declName) |>.isNone
     else
       return true

src/Lean/DefEqAttrib.lean

@@ -56,7 +56,7 @@ Marks the theorem as a definitional equality.
 The theorem must be an equality that holds by `rfl`. This allows `dsimp` to use this theorem
 when rewriting.
 
-A theorem with with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`.
+A theorem with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`.
 To avoid this behavior, write `:= (rfl)` instead.
 
 The attribute should be given before a `@[simp]` attribute to have effect.

src/Lean/Elab/Coinductive.lean

@@ -345,7 +345,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
         | throwError "expected to be quantifier"
       let motiveMVar ← mkFreshExprMVar type
       /-
-        We intro all the indices and the occurence of the coinductive predicate
+        We intro all the indices and the occurrence of the coinductive predicate
       -/
       let (fvars, subgoal) ← motiveMVar.mvarId!.introN (info.numIndices + 1)
       subgoal.withContext do
@@ -373,7 +373,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
           -/
           let originalCasesOn := mkAppN originalCasesOn indices
           /-
-            The next argument is the occurence of the coinductive predicate.
+            The next argument is the occurrence of the coinductive predicate.
             The original `casesOn` of the flat inductive mentions it in
             unrolled form, so we need to rewrite it.
           -/
@@ -447,7 +447,7 @@ public def elabCoinductive (coinductiveElabData : Array CoinductiveElabData) : T
   let consts := namesAndTypes.map fun (name, _) => (mkConst name levelParams)
   /-
     We create values of each of PreDefinitions, by taking existential (see `Meta.SumOfProducts`)
-    form of the associated flat inductives and applying paramaters, as well as recursive calls
+    form of the associated flat inductives and applying parameters, as well as recursive calls
     (with their parameters passed).
   -/
   let preDefVals ← forallBoundedTelescope infos[0]!.type originalNumParams fun params _ => do

src/Lean/Elab/Do/Legacy.lean

@@ -201,7 +201,7 @@ def AltExpr.vars (alt : AltExpr σ) : Array Var := Id.run do
     `vars` is the array of variables declared by it, and `cont` is the next instruction in the `do` code block.
     `vars` is an array since we have declarations such as `let (a, b) := s`.
 
-  - `reassign` is an reassignment-like `doElem` (e.g., `x := x + 1`).
+  - `reassign` is a reassignment-like `doElem` (e.g., `x := x + 1`).
 
   - `joinpoint` is a join point declaration: an auxiliary `let`-declaration used to represent the control-flow.
 

src/Lean/Elab/PreDefinition/FixedParams.lean

@@ -462,7 +462,7 @@ def FixedParamPerms.erase  (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
       assert! paramIdx < mapping.size
       if let some fixedParamIdx := mapping[paramIdx]! then
         mask := mask.set! fixedParamIdx true
-  -- Take the transitive closure under under `fixedParamPerms.revDeps`.
+  -- Take the transitive closure under `fixedParamPerms.revDeps`.
   let mut changed := true
   while changed do
     changed := false

src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -15,7 +15,7 @@ This module contains the types
 * `IndGroupInfo`, a variant of `InductiveVal` with information that
    applies to a whole group of mutual inductives and
 * `IndGroupInst` which extends `IndGroupInfo` with levels and parameters
-   to indicate a instantiation of the group.
+   to indicate an instantiation of the group.
 
 One purpose of this abstraction is to make it clear when a function operates on a group as
 a whole, rather than a specific inductive within the group.
@@ -50,7 +50,7 @@ partial def IndGroupInfo.brecOnName (info : IndGroupInfo) (idx : Nat) : Name :=
       info.brecOnName 0 |>.appendIndexAfter j
 
 /--
-An instance of an mutually inductive group of inductives, identified by the `all` array
+An instance of a mutually inductive group of inductives, identified by the `all` array
 and the level and expressions parameters.
 
 For example this distinguishes between `List α` and `List β` so that we will not even attempt

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -54,7 +54,7 @@ This is a hack to fix fallout from #8519, where a non-exposed wfrec definition `
 in a module would cause `foo.eq_def` to be defined eagerly and privately,
 but it should still be visible from non-module files.
 
-So we create a unfold equation generator that aliases an existing private `eq_def` to
+So we create an unfold equation generator that aliases an existing private `eq_def` to
 wherever the current module expects it.
 -/
 def copyPrivateUnfoldTheorem : GetUnfoldEqnFn := fun declName => do

src/Lean/Environment.lean

@@ -2138,7 +2138,7 @@ sufficient for our purposes.
 We may have to revise this design decision and eagerly generate equational theorems when
 we implement the module system.
 
-Remark: we do not check whether the theorem `value` field match. This feature is useful and
+Remark: we do not check whether the theorem `value` field matches. This feature is useful and
 ensures the proofs for equational theorems do not need to be identical. This decision
 relies on the fact that theorem types are propositions, we have proof irrelevance,
 and theorems are (mostly) opaque in Lean. For `Acc.rec`, we may unfold theorems

src/Lean/LibrarySuggestions/Basic.lean

@@ -92,10 +92,10 @@ end FoldRelevantConstantsImpl
 @[implemented_by FoldRelevantConstantsImpl.foldUnsafe]
 public opaque foldRelevantConstants {α : Type} (e : Expr) (init : α) (f : Name → α → MetaM α) : MetaM α := pure init
 
-/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstants (e : Expr) : MetaM (Array Name) := foldRelevantConstants e #[] (fun n ns => return ns.push n)
 
-/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstantsAsSet (e : Expr) : MetaM NameSet := foldRelevantConstants e ∅ (fun n ns => return ns.insert n)
 
 end Lean.Expr

src/Lean/LocalContext.lean

@@ -598,7 +598,7 @@ def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) (usedLetOnly : B
 @[inline] def all (lctx : LocalContext) (p : LocalDecl → Bool) : Bool :=
   Id.run <| lctx.allM (pure <| p ·)
 
-/-- If option `pp.sanitizeNames` is set to `true`, add tombstone to shadowed local declaration names and ones contains macroscopes. -/
+/-- If option `pp.sanitizeNames` is set to `true`, add tombstone to shadowed local declaration names and ones containing macroscopes. -/
 def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext := do
   let st ← get
   if !getSanitizeNames st.options then pure lctx else

src/Lean/Meta/Match/Match.lean

@@ -22,9 +22,9 @@ import Lean.Meta.Match.NamedPatterns
 
 /-!
 This module implements the backend of match compilation. The elaborator has already elaborated
-the patterns and the the expected type of the matcher is known.
+the patterns and the expected type of the matcher is known.
 
-The match compilation task is represented as a `Problem`, which is then processed interatively by
+The match compilation task is represented as a `Problem`, which is then processed iteratively by
 the `process` function. It has various “moves” which it tries in a particular order, to make progress
 on the problem, possibly splitting it.
 

src/Lean/Meta/PProdN.lean

@@ -150,7 +150,7 @@ def projM (n i : Nat) (e : Expr) : MetaM Expr := do
 /--
 Packs multiple type-forming lambda expressions taking the same parameters using `PProd`.
 
-The parameter `type` is the common type of the these expressions
+The parameter `type` is the common type of these expressions
 
 For example
 ```

src/Lean/Meta/Sym/Pattern.lean

@@ -213,7 +213,7 @@ partial def process (p : Expr) (e : Expr) : UnifyM Bool := do
     /-
     **Note**: Most patterns do not have free variables since they are created from
     top-level theorems. That said, some user may want to create patterns using local hypotheses, and they
-    may contain free variables. This is not the common case. So, we just push to pending an continue.
+    may contain free variables. This is not the common case. So, we just push to pending and continue.
     -/
     pushPending p e
     return true

src/Lean/Meta/Tactic/Grind/AC/Types.lean

@@ -117,7 +117,7 @@ structure State where
   -/
   structs : Array Struct := {}
   /--
-  Mapping from operators to its "operator id". We cache failures using `none`.
+  Mapping from operators to their "operator id". We cache failures using `none`.
   `opIdOf[op]` is `some id`, then `id < structs.size`. -/
   opIdOf : PHashMap ExprPtr (Option Nat) := {}
   /--

src/Lean/Meta/Tactic/Grind/Order/Types.lean

@@ -134,7 +134,7 @@ structure State where
   /-- Order structures detected. -/
   structs : Array Struct := {}
   /--
-  Mapping from types to its "structure id". We cache failures using `none`.
+  Mapping from types to their "structure id". We cache failures using `none`.
   `typeIdOf[type]` is `some id`, then `id < structs.size`. -/
   typeIdOf : PHashMap ExprPtr (Option Nat) := {}
   /-- Mapping from expressions/terms to their structure ids. -/

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -295,7 +295,7 @@ def withSplitSource [MonadControlT GrindM m] [Monad m] (splitSource : SplitSourc
 def getConfig : GrindM Grind.Config :=
   return (← readThe Context).config
 
-/-- Returns extension states associate with `grind` attributes in use -/
+/-- Returns extension states associated with `grind` attributes in use -/
 def getExtensions : GrindM Grind.ExtensionStateArray :=
   return (← readThe Context).extensions
 
@@ -1211,7 +1211,7 @@ def isEqv (a b : Expr) : GoalM Bool := do
     let some nb ← getENode? b | return false
     return isSameExpr na.root nb.root
 
-/-- Returns `true` if the root of its equivalence class. -/
+/-- Returns `true` if `e` is the root of its equivalence class. -/
 def isRoot (e : Expr) : GoalM Bool := do
   let some n ← getENode? e | return false -- `e` has not been internalized. Panic instead?
   return isSameExpr n.root e
@@ -1242,7 +1242,7 @@ def getRootENode? (e : Expr) : GoalM (Option ENode) := do
   let some n ← getENode? e | return none
   getENode? n.root
 /--
-Returns `true` if the ENode associate with `e` has support for function equality
+Returns `true` if the ENode associated with `e` has support for function equality
 congruence closure. See `Grind.Config.funCC` for additional details.
 -/
 def useFunCC (e : Expr) : GoalM Bool :=
@@ -1419,7 +1419,7 @@ For each equality `b = c` in `parents`, executes `k b c` IF
       else
         k b c
 
-/-- Returns `true` is `e` is the root of its congruence class. -/
+/-- Returns `true` if `e` is the root of its congruence class. -/
 def isCongrRoot (e : Expr) : GoalM Bool := do
   return (← getENode e).isCongrRoot
 

src/Lean/Meta/WHNF.lean

@@ -210,7 +210,7 @@ private def isWFRec (declName : Name) : Bool :=
 /--
 Helper method for `reduceRec`.
 We use it to ensure we don't expose `Nat.add` when reducing `Nat.rec`.
-We we use the following trick, if `e` can be expressed as an offset `(a, k)` with `k > 0`,
+We use the following trick: if `e` can be expressed as an offset `(a, k)` with `k > 0`,
 we create a new expression `Nat.succ e'` where `e'` is `a` for `k = 1`, or `a + (k-1)` for `k > 1`.
 See issue #3022
 -/

src/Lean/Parser/Basic.lean

@@ -151,7 +151,7 @@ def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s =>
 
 /-- Generate an error at the position saved with the `withPosition` combinator.
    If `delta == true`, then it reports at saved position+1.
-   This useful to make sure a parser consumed at least one character.  -/
+   This is useful to make sure a parser consumed at least one character.  -/
 @[builtin_doc] def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
   fn := errorAtSavedPosFn msg delta
 }

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -884,7 +884,7 @@ binder group `(d e ...)` as determined by `shouldGroupWithNext`. We cannot do gr
 inside-out, on the Syntax level, because it depends on comparing the Expr binder types.
 
 The `allNames` set is used to make sure names in the same `fun` binders are unique.
-Users have reported than `fun x x x => x` is confusing.
+Users have reported that `fun x x x => x` is confusing.
 -/
 private partial def delabBinders (allNames : NameSet) (curNames : Array Syntax) (dep ppTypes : Bool)
     (delabBody : NameSet → Delab)

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -33,7 +33,7 @@ def findCompletionCmdDataAtPos
     : ServerTask (Option (Syntax × Elab.InfoTree)) :=
   -- `findCmdDataAtPos` may produce an incorrect snapshot when `pos` is in whitespace.
   -- However, most completions don't need trailing whitespace at the term level;
-  -- synthetic completions are the only notions of completion that care care about whitespace.
+  -- synthetic completions are the only notions of completion that care about whitespace.
   -- Synthetic tactic completion only needs the `ContextInfo` of the command, so any snapshot
   -- will do.
   -- Synthetic field completion in `{ }` doesn't care about whitespace;

src/Lean/Shell.lean

@@ -108,7 +108,7 @@ opaque Internal.enableDebug (tag : @& String) : BaseIO Unit
 /--
 Lean's short version string (i.e., what is printed by `lean --short-version`).
 
-This is the Lean equivalent of of the C++ `LEAN_VERSION_STRING` / `g_short_version_string`.
+This is the Lean equivalent of the C++ `LEAN_VERSION_STRING` / `g_short_version_string`.
 -/
 def shortVersionString : String :=
   if version.specialDesc ≠ "" then

src/runtime/libuv.h

@@ -18,7 +18,6 @@ Author: Markus Himmel, Sofia Rodrigues
 #include "runtime/object.h"
 #include "runtime/thread.h"
 #include "runtime/allocprof.h"
-#include "runtime/object.h"
 
 namespace lean {
 

src/runtime/object_ref.h

@@ -206,7 +206,7 @@ inline object * mk_except_error_string(char const * err) {
     return r;
 }
 
-/* Given `o` representing a Lean value of type `Except String A`, return `T` an smart pointer
+/* Given `o` representing a Lean value of type `Except String A`, return `T` a smart pointer
    that encapsulates `A` values or throw an exception */
 template<typename T> T get_except_value(obj_arg o) {
     if (cnstr_tag(o) == 1) {