chore: fix spelling mistakes in tests (#5439)

Co-authored-by: euprunin <euprunin@users.noreply.github.com>

src/lake/examples/scripts/expected.out

@@ -14,8 +14,8 @@ Greet the entity with the given name. Otherwise, greet the whole world.
 Hello from Dep!
 Hello from Dep!
 Goodbye!
-error: unknown script nonexistant
-error: unknown script nonexistant
+error: unknown script nonexistent
+error: unknown script nonexistent
 dep/hello
 scripts/say-goodbye
 scripts/greet

src/lake/examples/scripts/test.sh

@@ -18,8 +18,8 @@ $LAKE script run dep/hello | tee -a produced.out
 # Test that non-indentifier names work
 # https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Running.20.60lake.60.20scripts.20from.20the.20command.20line/near/446944450
 $LAKE script run say-goodbye | tee -a produced.out
-($LAKE script run nonexistant 2>&1 | tee -a produced.out) && exit 1 || true
-($LAKE script doc nonexistant 2>&1 | tee -a produced.out) && exit 1 || true
+($LAKE script run nonexistent 2>&1 | tee -a produced.out) && exit 1 || true
+($LAKE script doc nonexistent 2>&1 | tee -a produced.out) && exit 1 || true
 $LAKE scripts | tee -a produced.out
 $LAKE run | tee -a produced.out
 

src/lake/tests/init/test.sh

@@ -13,7 +13,7 @@ fi
 LAKE1=${LAKE:-../../../.lake/build/bin/lake}
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
-# Test `new` and `init` with bad template/langauge (should error)
+# Test `new` and `init` with bad template/language (should error)
 
 ($LAKE new foo bar 2>&1 && exit 1 || true) | grep --color "unknown package template"
 ($LAKE new foo .baz 2>&1 && exit 1 || true) | grep --color "unknown configuration language"

src/lake/tests/toml/tests/valid/comment/everywhere.toml

@@ -7,7 +7,7 @@
 [group] # Comment
 answer = 42 # Comment
 # no-extraneous-keys-please = 999
-# Inbetween comment.
+# In between comment.
 more = [ # Comment
   # What about multiple # comments?
   # Can you handle it?

tests/compiler/trie.lean

@@ -43,11 +43,11 @@ def T.insert : T → String → T := fun (t,a) s =>
 def Array.sorted : Array String → Array String := fun a =>
   a.qsort (fun s1 s2 => s1 < s2)
 
-/-- The intendend semanics of `Trie.findPrefix` -/
+/-- The intended semanics of `Trie.findPrefix` -/
 def Array.findPrefix : Array String → String → Array String := fun a s =>
   a.filter (fun s' => s.isPrefixOf s')
 
-/-- The intendend semanics of `Trie.matchPrefix`: Longest prefix found in trie -/
+/-- The intended semanics of `Trie.matchPrefix`: Longest prefix found in trie -/
 def Array.matchPrefix : Array String → String → Option String := fun a s => Id.run do
   for i in List.reverse (List.range (s.length + 1)) do
     let pfix := s.take i

tests/lean/1007.lean

@@ -52,5 +52,5 @@ example : SemiHilbert (Trait.R ℝ) ℝ := by infer_instance
 -- set_option pp.explicit true in
 -- set_option trace.Meta.synthInstance true in
 
--- This should not timeout but failt in finite number of steps like in Lean 3
+-- This should not timeout but fail in finite number of steps like in Lean 3
 example : IsLin  (λ (x : ℝ) => sum λ i : Fin n => norm x) := by infer_instance

tests/lean/277a.lean

@@ -1,4 +1,4 @@
 set_option hygiene false
-infixl:67 " <>< "  => nonexistant
+infixl:67 " <>< "  => nonexistent
 
 #eval (1 <>< 11 : UInt64)

tests/lean/277a.lean.expected.out

@@ -1,3 +1,3 @@
-277a.lean:4:7-4:15: error: unknown identifier 'nonexistant'
+277a.lean:4:7-4:15: error: unknown identifier 'nonexistent'
 277a.lean:4:0-4:25: error: cannot evaluate expression that depends on the `sorry` axiom.
 Use `#eval!` to evaluate nevertheless (which may cause lean to crash).

tests/lean/bool_simp.lean

@@ -125,7 +125,7 @@ variable [Decidable u]
 #check_simp (b ∧  b) ~> (b : Prop)
 #check_simp (b && b) ~> b
 
--- Cancelation
+-- Cancellation
 #check_simp (u ∧ ¬u)  ~> False
 #check_simp (¬u ∧ u)  ~> False
 #check_simp (b && ¬b) ~> false

tests/lean/guessLex.lean

@@ -155,13 +155,13 @@ def oddNat : OddNat → Nat
   | ⟨.succ n⟩ => oddNat ⟨n⟩
 decreasing_by decreasing_tactic
 
--- Shadowing `sizeOf`, as a varying paramter
+-- Shadowing `sizeOf`, as a varying parameter
 def shadowSizeOf1 (sizeOf : Nat) : OddNat → Nat
   | ⟨0⟩ => 0
   | ⟨.succ n⟩ => shadowSizeOf1 (sizeOf + 1) ⟨n⟩
 decreasing_by decreasing_tactic
 
--- Shadowing `sizeOf`, as a fixed paramter
+-- Shadowing `sizeOf`, as a fixed parameter
 def shadowSizeOf2 (sizeOf : Nat) : OddNat → Nat → Nat
   | ⟨0⟩, m => m
   | ⟨.succ n⟩, m => shadowSizeOf2 sizeOf ⟨n⟩ m
@@ -215,7 +215,7 @@ end
 end MutualNotNat2
 
 namespace MutualNotNat3
--- A varant of the above, but where the type of the parameter refined to `Nat`.
+-- A variant of the above, but where the type of the parameter refined to `Nat`.
 -- Previously `GuessLex` was inferring the `SizeOf` instance based on the type of the
 -- *concrete* parameter or argument, which was wrong.
 -- The inference needs to be based on the parameter type in the function's signature.

tests/lean/implicitArgumentError.lean

@@ -2,7 +2,7 @@
 In the past, when an implicit argument couldn't be synthesized, the name of the argument got lost during elaboration.
 Now it is saved and added to the error message.
 
-In this exaple, that is 'n'.
+In this example, that is 'n'.
 -/
 
 def foo {n : Nat} := 2*n

tests/lean/indUsingTerm.lean

@@ -107,7 +107,7 @@ end
 -- NB: A.rec is configured as elab_as_elim,
 -- but in `using` it should not matter
 
--- For comparision, a copy without that attribute
+-- For comparison, a copy without that attribute
 noncomputable def A_rec := @A.rec
 
 set_option linter.unusedVariables false

tests/lean/interactive/catHover.lean

@@ -1,4 +1,4 @@
-/-- Index syntax categoy -/
+/-- Index syntax category -/
 declare_syntax_cat index
 
                                --v textDocument/hover

tests/lean/interactive/catHover.lean.expected.out

@@ -20,7 +20,7 @@
  {"start": {"line": 4, "character": 24}, "end": {"line": 4, "character": 29}},
  "contents":
  {"value":
-  "```lean\nLean.Parser.Category.index : Lean.Parser.Category\n```\n***\nIndex syntax categoy ",
+  "```lean\nLean.Parser.Category.index : Lean.Parser.Category\n```\n***\nIndex syntax category ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///catHover.lean"},
  "position": {"line": 12, "character": 16}}

tests/lean/run/2846.lean

@@ -47,7 +47,7 @@ def foo' (n n : Nat) (a : Fin ((by clear n; exact n) + 1)) : Fin (n + 1) := 0
 #guard_msgs in #check foo'
 
 /-!
-Named argument after inaccesible name, still stays after the colon.
+Named argument after inaccessible name, still stays after the colon.
 But, it does not print using named pi notation since this is not a dependent type.
 -/
 def foo'' : String → (needle : String) → String := fun _ yo => yo

tests/lean/run/3643.lean

@@ -1,7 +1,7 @@
 
 import Lean
 /-!
-# Make sure 'ext' attribute works in conjuction with local/scoped
+# Make sure 'ext' attribute works in conjunction with local/scoped
 -/
 
 section Ex0

tests/lean/run/DVec.lean

@@ -5,7 +5,7 @@ def Vec (α : Type _) (n : Nat) : Type _
 abbrev TypeVec : Nat → Type _
   := Vec (Type _)
 
-/-- A dependent vector is a heterogenous list of statically known size -/
+/-- A dependent vector is a heterogeneous list of statically known size -/
 def DVec {n : Nat} (αs : TypeVec n) : Type _
   := (i : Fin n) → (αs i)
 

tests/lean/run/bv_math_lit_perf.lean

@@ -17,7 +17,7 @@ def f (x : BitVec 32) : Nat :=
   | _      => 1000
 
 -- Generate the equational lemmas ahead of time, to avoid going
--- over the hearbeat limit below
+-- over the heartbeat limit below
 #guard_msgs(drop all) in
 #print equations f
 

tests/lean/run/eqnsProjections.lean

@@ -1,5 +1,5 @@
 /-!
-This test should catch intentional or accidential changes to how projections are rewritten by
+This test should catch intentional or accidental changes to how projections are rewritten by
 various tactics
 -/
 

tests/lean/run/funind_structural_mutual.lean

@@ -32,7 +32,7 @@ info: Tree.size.induct.{u_1} {α : Type u_1} (motive_1 : Tree α → Prop) (moti
 #check Tree.size.induct
 
 
--- Recursion over nested inductive, functions in the “wrong” order (auxillary first)
+-- Recursion over nested inductive, functions in the “wrong” order (auxiliary first)
 
 mutual
 def Tree.size_aux' : List (Tree α) → Nat

tests/lean/run/funind_tests.lean

@@ -473,7 +473,7 @@ end AsPattern
 
 namespace GramSchmidt
 
--- this tried to repoduce a problem with gramSchmidt,
+-- this tried to reproduce a problem with gramSchmidt,
 -- with more proofs from `simp` abstracting over the IH.
 -- I couldn't quite reproduce it, but let's keep it.
 

tests/lean/run/issue4146.lean

@@ -16,7 +16,7 @@ termination_by n
 -- NB: The induction theorem has both `h` in scope, as its original type mentioning `x`,
 -- and a refined `h` mentioning `m+1`.
 -- The former is redundant here, but will we always know that?
--- No HEq betwen the two `h`s due to proof irrelevance
+-- No HEq between the two `h`s due to proof irrelevance
 
 /--
 info: bar.induct (motive : Nat → Prop) (case1 : motive 0)

tests/lean/run/issue4671.lean

@@ -20,7 +20,7 @@ def A.size (acc n : Nat) : A n → Nat
   | .b a' => 1 + A.size (acc + 1) n a'
 termination_by structural a => a
 
--- Another instance repoted on Zulip at
+-- Another instance reported on Zulip at
 -- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20Doubly-nested.20inductive/near/451204850
 
 inductive Xn (e : Sigma.{0} (· → Type)) (α : Type) : Nat → Type where

tests/lean/run/issue5027.lean

@@ -6,7 +6,7 @@ inductive Term (α: Type): Type where
 def height (f: Term α): Nat :=
   let rec max_height (a: Array (Term α)) (i: Nat) (m: Nat): Nat :=
     if h: i < a.size then
-      -- The recusive call to height used to fail because of a too weak
+      -- The recursive call to height used to fail because of a too weak
       -- array_get_dec
       max_height a (i + 1) (max (height a[i]) m)
     else

tests/lean/run/match_lit_fin_cover.lean

@@ -1,5 +1,5 @@
 /-
-Test for match-expression when we conver all possible
+Test for match-expression when we cover all possible
 values of a `Fin` or `BitVec` type.
 -/
 

tests/lean/run/repr_empty.lean

@@ -5,7 +5,7 @@ While it may seem unnecessary to have Repr, it prevents the automatic derivation
 of Repr for other types when `Empty` is used as a type parameter.
 
 This is a simplified version of an example from the "Functional Programming in Lean" book.
-The Empty type is used to exlude the `other` constructor from the `Prim` type.
+The Empty type is used to exclude the `other` constructor from the `Prim` type.
 -/
 
 inductive Prim (special : Type) where

tests/lean/run/simprocNat.lean

@@ -110,12 +110,12 @@ variable (a b : Nat)
 #check_simp (a + 1000) != (b +  400) ~> a + 600 != b
 #check_simp (a +  400) != (b + 1000) ~> a != b + 600
 
-/-! Alterate instance tests
+/-! Alternate instance tests
 
 These check that the simplification rules will matching
-offets still trigger even when the expression for the
+offsets still trigger even when the expression for the
 index is definition equal but not syntactically equal
-to the defualt instance.
+to the default instance.
 
 This can be relevant in Mathlib when rewriting using
 theorems involving algebraic hierarchy classes.

tests/lean/run/structuralOverNested.lean

@@ -11,7 +11,7 @@ end
 
 example : Tree.list_size (t :: ts) = t.size + Tree.list_size ts := rfl
 
--- If we only look at the nested type at a finite depth we don't need an auxillary definition:
+-- If we only look at the nested type at a finite depth we don't need an auxiliary definition:
 
 def Tree.isList : Tree → Bool
   | .node [] => true

tests/lean/run/trace.lean

@@ -44,7 +44,7 @@ do withTraceNode `module.slow (fun _ => return m!"slow: {slow b}") do {
 def run (x : M Unit) : M Unit :=
 withReader
   (fun ctx =>
-    -- Try commeting/uncommeting the following `setBool`s
+    -- Try commenting/uncommeting the following `setBool`s
     let opts := ctx.options;
     let opts := opts.setBool `trace.module true;
     -- let opts := opts.setBool `trace.module.aux false;

tests/pkg/user_attr/UserAttr/Tst.lean

@@ -26,7 +26,7 @@ def getFooAttrInfo? (declName : Name) : CoreM (Option (Nat × Bool)) :=
 @[my_simp] theorem g_eq : g x = x + 1 := rfl
 
 example : f x + g x = 2*x + 3 := by
-  fail_if_success simp_arith -- does not appy f_eq and g_eq
+  fail_if_success simp_arith -- does not apply f_eq and g_eq
   simp_arith [f, g]
 
 example : f x + g x = 2*x + 3 := by

tests/playground/bool_exhaust_test.lean

@@ -448,7 +448,7 @@ behavior.
 
 General goals for simp are that the normal forms are sensible to a wide
 range of users and that it performs well.  We also strive for Mathlib
-compatiblity.
+compatibility.
 -/
 
 inductive BoolType where

tests/playground/eval.lean

@@ -26,7 +26,7 @@ def eval (fName : Name) (n : Nat) : IO Nat :=
 do m ← simpleFnTable.get,
    match m.find fName with
    | some f := pure $ f n
-   | none   := throw (IO.userError "unknow function")
+   | none   := throw (IO.userError "unknown function")
 
 def main (xs : List String) : IO Unit :=
 do [f, x] ← pure xs | throw "invalid number of arguments",