doc(All): Spelling fixes found using codespell (#538)

Arleee1 · web-flow · commit 3716b278483e · 2026-05-03T08:50:05.000Z
Fixes a few typos found using codespell
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -98,7 +98,7 @@ instructions on how to run these locally.
 ## Pull Request Titles
 
 It is required that pull request titles begun with one of the following categories followed by a
-colon: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`. These may optionally be followed by a 
+colon: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`. These may optionally be followed by a
 parenthetical containing what area of the library the PR is working on.
 
 ## Testing
@@ -234,7 +234,7 @@ Reusable APIs that support many concrete algorithms.
 
 We aim at formalising a number of logics of different kinds, including linear logic, modal logics, etc.
 
-We welcome proofs of logical equivalences and metatheoretical results such as identity expansion, cut elimiation, etc.
+We welcome proofs of logical equivalences and metatheoretical results such as identity expansion, cut elimination, etc.
 
 Examples of interesting logics include:
 - Linear logic
diff --git a/Cslib/Computability/Automata/NA/BuchiInter.lean b/Cslib/Computability/Automata/NA/BuchiInter.lean
@@ -54,14 +54,14 @@ noncomputable def interNA (na : (i : Bool) → NA (State i) Symbol)
     (acc : (i : Bool) → Set (State i)) : NA ((Π i, State i) × Bool) Symbol :=
   (iProd na).addHist histStart (histTrans acc)
 
-/-- The overall accepting conditon of the intersection automaton. -/
+/-- The overall accepting condition of the intersection automaton. -/
 @[scoped grind =]
 def interAccept (acc : (i : Bool) → Set (State i)) : Set ((Π i, State i) × Bool) :=
   interAcc false acc ∪ interAcc true acc
 
 variable {na : (i : Bool) → NA (State i) Symbol} {acc : (i : Bool) → Set (State i)}
 
-/-- If the intersection automaton sees one accepting condtion infinitely many times,
+/-- If the intersection automaton sees one accepting condition infinitely many times,
 then it sees the other accepting condition infinitely many times as well. -/
 lemma inter_freq_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((Π i, State i) × Bool)}
     {i : Bool} (h_run : (interNA na acc).Run xs ss) (h_inf : ∃ᶠ k in atTop, ss k ∈ interAcc i acc) :
@@ -76,7 +76,7 @@ lemma inter_freq_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((Π i,
     · apply Frequently.mono h_inf
       grind
 
-/-- If the intersection automaton sees the accepting condtions of both component automata
+/-- If the intersection automaton sees the accepting conditions of both component automata
 infinitely many times, then its own accepting condition also happens infinitely many times. -/
 lemma inter_freq_comp_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((Π i, State i) × Bool)}
     (h_run : (interNA na acc).Run xs ss)
diff --git a/Cslib/Computability/Automata/NA/Loop.lean b/Cslib/Computability/Automata/NA/Loop.lean
@@ -20,7 +20,7 @@ open scoped Run LTS
 
 variable {Symbol State : Type*}
 
-/-- `na.loop` mimics `na`, but can nondeterministically decide to "loop back" by identifing
+/-- `na.loop` mimics `na`, but can nondeterministically decide to "loop back" by identifying
 an accepting state of `na` with a starting state of `na`.  This identification is achieved
 via a new dummy state `()`, which is the sole starting state and the sole accepting state
 of `na.loop`. -/
diff --git a/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean b/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean
@@ -121,7 +121,7 @@ private lemma good_selections_exist :
 
 /-- If the edges of an infinite complete graph is assigned a finite number of colors,
 then there must exist a color `c` and an infinite set `s` of vertices such that the edge
-beteen any two vertices of `s` is assigned the same color `c`. -/
+between any two vertices of `s` is assigned the same color `c`. -/
 theorem infinite_graph_ramsey :
     ∃ c : Color, ∃ s : Set Vertex, s.Infinite ∧
       ∀ e : Finset Vertex, e.card = 2 → ↑e ⊆ s → color e = c := by
diff --git a/Cslib/Foundations/Data/Nat/Segment.lean b/Cslib/Foundations/Data/Nat/Segment.lean
@@ -16,7 +16,7 @@ public import Mathlib.Data.Nat.Nth
 Given a strictly monotonic function `f : ℕ → ℕ` and `k : ℕ` with `k ≥ f 0`,
 `Nat.segment f k` is the unique `m : ℕ` such that `f m ≤ k < f (k + 1)`.
 `Nat.segment f k` is defined to be 0 for `k < f 0`.
-This file defines `Nat.segment` and proves various properties aboout it.
+This file defines `Nat.segment` and proves various properties about it.
 -/
 
 @[expose] public section
diff --git a/Cslib/Foundations/Data/OmegaSequence/Defs.lean b/Cslib/Foundations/Data/OmegaSequence/Defs.lean
@@ -16,7 +16,7 @@ public import Mathlib.Logic.Function.Iterate
 An `ωSequence α` is an infinite sequence of elements of `α`.  It is basically
 a wrapper around the type `ℕ → α` which supports the dot-notation and
 the analogues of many familiar API functions of `List α`.  In particular,
-the element at postion `n : ℕ` of `s : ωSequence α` is obtained using the
+the element at position `n : ℕ` of `s : ωSequence α` is obtained using the
 function application notation `s n`.
 
 In this file we define `ωSequence` and its API functions.
diff --git a/Cslib/Foundations/Data/OmegaSequence/Flatten.lean b/Cslib/Foundations/Data/OmegaSequence/Flatten.lean
@@ -149,7 +149,7 @@ theorem flatten_drop [Inhabited α]
     (ls.drop n).flatten = ls.flatten.drop (ls.cumLen n) :=
   (flatten_take_drop h_ls n).2
 
-/-- `ls n` is the segement from position `ls.cumLen n` to position `ls.cumLen (n + 1) - 1`
+/-- `ls n` is the segment from position `ls.cumLen n` to position `ls.cumLen (n + 1) - 1`
 of `ls.flatten` -/
 @[simp, scoped grind =]
 theorem extract_flatten [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k).length > 0)
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
@@ -183,7 +183,7 @@ lemma map_subst (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ'
 
 variable [HasFresh Var]
 
-/-- A well-formed context is unchaged by substituting for a free key. -/
+/-- A well-formed context is unchanged by substituting for a free key. -/
 lemma map_subst_nmem (Γ : Env Var) (X : Var) (σ : Ty Var) (wf : Γ.Wf) (nmem : X ∉ Γ.dom) :
     Γ = Γ.map_val (·[X:=σ]) := by
   induction wf <;> grind [Ty.Wf.nmem_fv, Binding.subst_fresh]
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
@@ -91,7 +91,7 @@ theorem progress {t : Term Var} {τ : Ty Base} (ht : [] ⊢ t ∶ τ) : t.Value
     cases ih_l with
     -- if the lhs is a value, beta reduce the application
     | inl val => cases val with | abs M _ => use M ^ N, by grind
-    -- otherwise, propogate the step to the lhs of the application
+    -- otherwise, propagate the step to the lhs of the application
     | inr step =>
       obtain ⟨M', _⟩ := step
       use M'.app N
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
@@ -14,7 +14,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 
-/-! Strong normalization (termination) for full beta-reduction of simply typed lamba calulus. -/
+/-! Strong normalization (termination) for full beta-reduction of simply typed lambda calculus. -/
 
 @[expose] public section
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -174,7 +174,7 @@ lemma step_subst_cong_r {x : Var} (s t t' : Term Var) (step : t ⭢βᶠ t') (h_
 
 /- `step_subst_cong_r` can be generalized to multiple reductions `t ↠βᶠ t'`.
    This requires s to be locally closed, locally closedness of t and t'
-   can be infered by the fact t reduces to t' -/
+   can be inferred by the fact t reduces to t' -/
 lemma steps_subst_cong_r {x : Var} (s t t' : Term Var) (step : t ↠βᶠ t') (h_lc : LC s) :
     (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by
   induction step with
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
@@ -28,7 +28,7 @@ open scoped Context
 
 variable {Var : Type u} {Base : Type v} [DecidableEq Var]
 
-/-- An environment in context of multi substition is a list of pairs of
+/-- An environment in context of multi substitution is a list of pairs of
     variable targets and terms to be substituted for that target -/
 abbrev Env (Var : Type u) := Context Var (Term Var)
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -10,7 +10,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 
-/-! Strong normalization (termination) for full beta-reduction of untyped lamba calulus. -/
+/-! Strong normalization (termination) for full beta-reduction of untyped lambda calculus. -/
 
 @[expose] public section
 
diff --git a/Cslib/Logics/HML/Basic.lean b/Cslib/Logics/HML/Basic.lean
@@ -108,7 +108,7 @@ def Proposition.denotation (a : Proposition Label) (lts : LTS State Label)
   | .diamond μ a => {s | ∃ s', lts.Tr s μ s' ∧ s' ∈ a.denotation lts}
   | .box μ a => {s | ∀ s', lts.Tr s μ s' → s' ∈ a.denotation lts}
 
-/-- The theory of a state is the set of all propositions that it satifies. -/
+/-- The theory of a state is the set of all propositions that it satisfies. -/
 abbrev theory (lts : LTS State Label) (s : State) : Set (Proposition Label) :=
   {a | Satisfies lts s a}
 
diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean
@@ -18,7 +18,7 @@ open_scoped_all Cslib
   (This documentation and test is adapted from Mathlib.)
 
   Exceptions may be specified here using `#grind_lint skip`. This should be kept minimal, and some
-  of these were added upon the inital commit of this test. PRs removing exceptions are welcome.
+  of these were added upon the initial commit of this test. PRs removing exceptions are welcome.
 
   If this test fails, please modify newly introduced `grind` annotations to use the
   `grind_pattern ... where ...` syntax to add side conditions that will prevent the run-away.
diff --git a/CslibTests/Reduction.lean b/CslibTests/Reduction.lean
@@ -31,7 +31,7 @@ def term_rel : Term Var → Term Var → Prop := fun _ _ ↦ True
 example (a b : Term Var) : a ⭢β b := by
   simp
 
--- check that a "cannonical" notation also works
+-- check that a "canonical" notation also works
 @[reduction_sys, grind]
 def PredReduction' (a b : ℕ) : Prop := a = b + 1
 
