chore: fix spelling

Author: tom93

src/Init/Data/BitVec/Bitblast.lean

@@ -835,7 +835,7 @@ execution. -/
 structure DivModArgs (w : Nat) where
   /-- the numerator (aka, dividend) -/
   n : BitVec w
-  /-- the denumerator (aka, divisor)-/
+  /-- the denominator (aka, divisor)-/
   d : BitVec w
 
 /-- A `DivModState` is lawful if the remainder width `wr` plus the numerator width `wn` equals `w`,

src/Init/Data/Bool.lean

@@ -260,7 +260,7 @@ instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 
 theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y := by decide
 
-/-! ### coercision related normal forms -/
+/-! ### coercion related normal forms -/
 
 theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
     (a == b) = decide (a = b) := by

src/Init/Data/List/Lemmas.lean

@@ -77,7 +77,7 @@ Further results, which first require developing further automation around `Nat`,
 * `Init.Data.List.Nat.TakeDrop`: `List.take` and `List.drop`
 
 Also
-* `Init.Data.List.Monadic` for addiation lemmas about `List.mapM` and `List.forM`.
+* `Init.Data.List.Monadic` for additional lemmas about `List.mapM` and `List.forM`.
 
 -/
 

src/Init/Data/List/Sublist.lean

@@ -249,7 +249,7 @@ theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l
   | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _)
   | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)]
 
--- Only activative `eq_of_length` if we're already thinking about lengths.
+-- Only activate `eq_of_length` if we're already thinking about lengths.
 grind_pattern Sublist.eq_of_length => l₁ <+ l₂, length l₁, length l₂
 
 theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ :=

src/Init/Data/String/Basic.lean

@@ -1177,7 +1177,7 @@ position. -/
 def Slice.Pos.get? {s : Slice} (pos : s.Pos) : Option Char :=
   if h : pos = s.endPos then none else some (pos.get h)
 
-/-- Returns the byte at the given position in the string, or panicks if the position is the end
+/-- Returns the byte at the given position in the string, or panics if the position is the end
 position. -/
 @[expose]
 def Slice.Pos.get! {s : Slice} (pos : s.Pos) : Char :=

src/Init/Data/String/Decode.lean

@@ -529,7 +529,7 @@ public def assemble₂ (w x : UInt8) : Option Char :=
   else
     let r := assemble₂Unchecked w x
     if r < 0x80 then
-      none -- overlong encodinlg
+      none -- overlong encoding
     else
       some ⟨r, ?onemore⟩
 where finally

src/Init/Data/UInt/Basic.lean

@@ -517,7 +517,7 @@ protected def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (UI
 Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
 natural numbers. Usually accessed via the `<` operator.
 -/
--- These need to be exposed as `Init.Prelude` already has an instance for bootstrapping puproses and
+-- These need to be exposed as `Init.Prelude` already has an instance for bootstrapping purposes and
 -- they should be defeq
 @[expose] protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
 /--

src/Lean/Attributes.lean

@@ -250,7 +250,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
   afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   /--
   If set, entries are not resorted on export and `getParam?` will fall back to a linear instead of
-  binary search insde an imported module's entries.
+  binary search inside an imported module's entries.
   -/
   preserveOrder : Bool := false
   /--

src/Lean/Compiler/IR/LiveVars.lean

@@ -68,7 +68,7 @@ partial def visitFnBody (w : Index) : FnBody → M Bool
         -- Instead of marking the join points that we have already been visited, we permanently remove `j` from the context.
         set (ctx.eraseJoinPointDecl j) *> visitFnBody w b
       | none   =>
-        -- `j` must be a local join point. So do nothing since we have already visite its body.
+        -- `j` must be a local join point. So do nothing since we have already visited its body.
         pure false
   | .ret x =>
     visitArg w x

src/Lean/Elab/Coinductive.lean

@@ -72,7 +72,7 @@ builtin_initialize
   Note that at this point `PartialFixpoint` machinery applies the attributes and modifiers. We
   use the syntax references from the original `InductiveView`s and set them to those declarations.
 
-  Moreover, we have following theorem (generated by `generateEqLemmas`) that connets the coinductive
+  Moreover, we have following theorem (generated by `generateEqLemmas`) that connects the coinductive
   predicate to its flat inductive:
   ```
     info: infSeq.functor_unfold (α : Type) (r : α → α → Prop) (a✝ : α) : infSeq α r a✝ = infSeq._functor α r (infSeq α r) a✝
@@ -250,7 +250,7 @@ private def generateCoinductiveConstructor (infos : Array InductiveVal) (ctorSyn
       let newHole ← hole.replaceTargetEq rewriteResult.eNew rewriteResult.eqProof
 
       /-
-        Now, all it suffices is to call an approprate constructor of the flat inductive.
+        Now, all it suffices is to call an appropriate constructor of the flat inductive.
       -/
       let constructor := mkConst ctor.name levelParams
       let constructor := mkAppN constructor params
@@ -365,7 +365,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
         -- Then we apply the metavariable to the `casesOn` of the flat inductive
         let originalCasesOn := mkApp originalCasesOn motiveMVar
 
-        -- The next arguemnts of the `casesOn` are type indices
+        -- The next arguments of the `casesOn` are type indices
         forallBoundedTelescope goalType info.numIndices fun indices goalType => do
           /-
             The types do not change, so we just make free variables for them