doc: fix typos

doc/autobound.md

@@ -1,4 +1,4 @@
-## Auto Bound Implict Arguments
+## Auto Bound Implicit Arguments
 
 In the previous section, we have shown how implicit arguments make functions more convenient to use.
 However, functions such as `compose` are still quite verbose to define. Note that the universe

doc/decltypes.md

@@ -19,7 +19,7 @@ The type ``NewType`` consists of nothing more than the objects that are construc
 
 We will see below that the arguments to the constructors can include objects of type ``NewType``,
 subject to a certain "positivity" constraint, which guarantees that elements of ``NewType`` are built
-from the bottom up. Roughly speaking, each ``...`` can be any function type type constructed from ``NewType``
+from the bottom up. Roughly speaking, each ``...`` can be any function type constructed from ``NewType``
 and previously defined types, in which ``NewType`` appears, if at all, only as the "target" of the function type.
 
 We will provide a number of examples of inductive types. We will also consider slight generalizations of the scheme above,

doc/enum.md

@@ -148,7 +148,7 @@ def toString : Weekday -> String
 # end Weekday
 ```
 We can now prove the general theorem that ``next (previous d) = d`` for any weekday ``d``.
-The idea is perform a proof by cases using `match`, and rely on the fact for each constructor both
+The idea is to perform a proof by cases using `match`, and rely on the fact for each constructor both
 sides of the equality reduce to the same term.
 ```lean
 # inductive Weekday where

doc/fixing_tests.md

@@ -9,7 +9,7 @@ The later contains the expected output for the test file `bad_class.lean`.
 
 When the Lean source code or the standard library are modified, some of these
 tests break because the produced output is slightly different, and we have
-to reflect the changes int the `.lean.expected.out` files.
+to reflect the changes in the `.lean.expected.out` files.
 We should not blindly copy the new produced output since we may accidentally
 miss a bug introduced by recent changes.
 The test suite contains commands that allow us to see what changed in a convenient way.

doc/functions.md

@@ -106,8 +106,8 @@ def times2 x := x * 2
 #eval times2 <| add1 <| 100
 ```
 The result of the previous `#eval` commands is 202.
-The forward pipeline `|>` operatior takes a function and an argument and return a value.
-In constrat, the backward pipeline `<|` operator takes an argument and a function and returns a value.
+The forward pipeline `|>` operator takes a function and an argument and return a value.
+In contrast, the backward pipeline `<|` operator takes an argument and a function and returns a value.
 These operators are useful for minimizing the number of parentheses.
 ```lean
 def add1Times3FilterEven (xs : List Nat) :=

doc/lean3changes.md

@@ -16,7 +16,7 @@ The lambda expression notation has many new features that are not supported in L
 
 * Pattern matching
 
-In Lean 4, one can easily create new notation that abbreviates commonly used idioms. One of the them is a
+In Lean 4, one can easily create new notation that abbreviates commonly used idioms. One of them is a
 `fun` followed by a `match`. In the following examples, we define a few functions using `fun`+`match` notation.
 
 ```lean
@@ -43,7 +43,7 @@ def Sum.str : Option Nat → String :=
 
 In Lean 3 stdlib, we find many [instances](https://github.com/leanprover/lean/blob/master/library/init/category/reader.lean#L39) of the dreadful `@`+`_` idiom.
 It is often used when we the expected type is a function type with implicit arguments,
-and we have a constant (`reader_t.pure` in the example) which also takes implicit arguments. In Lean 4, the elaborator automatically introduces lambda's
+and we have a constant (`reader_t.pure` in the example) which also takes implicit arguments. In Lean 4, the elaborator automatically introduces lambdas
 for consuming implicit arguments. We are still exploring this feature and analyzing its impact, but the experience so far has been very positive. As an example,
 here is the example in the link above using Lean 4 implicit lambdas.
 
@@ -85,7 +85,7 @@ def id5 : {α : Type} → α → α :=
 
 * Sugar for simple functions
 
-In Lean 3, we can creating simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` As a placeholder. Here are a few examples:
+In Lean 3, we can create simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` As a placeholder. Here are a few examples:
 
 ```lean
 # namespace ex3
@@ -249,7 +249,7 @@ constant y : Nat
 ```
 
 We can instruct Lean to use a foreign function as the implementation for any constant or definition
-using the attribute `@[extern "foreign_function"]`. It is the user's reponsability to ensure the
+using the attribute `@[extern "foreign_function"]`. It is the user's responsibility to ensure the
 foreign implementation is correct.
 However, a user mistake here will only impact the code generated by Lean, and
 it will **not** compromise the logical soundness of the system.

doc/struct.md

@@ -123,7 +123,7 @@ def p : Point Nat :=
 
 ##  Inheritance
 
-We can *extend* existing structures by adding new fields. This feature allow us to simulate a form of *inheritance*.
+We can *extend* existing structures by adding new fields. This feature allows us to simulate a form of *inheritance*.
 
 ```lean
 structure Point (α : Type u) where

doc/syntax.md

@@ -23,7 +23,7 @@ postfix:max "⁻¹" => Inv.inv
 After the initial command name describing the operator kind (its "fixity"), we give the *parsing precedence* of the operator preceded by a colon `:`, then a new or existing token surrounded by double quotes (the whitespace is used for pretty printing), then the function this operator should be translated to after the arrow `=>`.
 
 The precedence is a natural number describing how "tightly" an operator binds to its arguments, encoding the order of operations.
-We can make this more precise by looking at the commands the commands above unfold to:
+We can make this more precise by looking at the commands above unfold to:
 
 ```lean
 notation:65 lhs " + " rhs:66 => HAdd.hAdd lhs rhs

doc/tactics.md

@@ -20,7 +20,7 @@ all local variables in scope.
 
 In the following example, we prove the same simple theorem using different tactics.
 The keyword `by` instructs Lean to use the tactic DSL to construct a term.
-Our initial goal is a hole with type `p ∨ q → q ∨ p`. We tactic `intro h`
+Our initial goal is a hole with type `p ∨ q → q ∨ p`. The tactic `intro h`
 fills this hole using the term `fun h => ?m` where `?m` is a new hole we need to solve.
 This hole has type `q ∨ p`, and the local context contains `h : p ∨ q`.
 The tactic `cases` fills the hole using `Or.casesOn h (fun h1 => ?m1) (fun h2 => ?m2)`

doc/typeclass.md

@@ -89,7 +89,7 @@ Note that `x + y` is notation for `Add.add x y` in Lean.
 The example above demonstrates how type classes are used to overload notation.
 Now, we explore another application. We often need an arbitrary element of a given type.
 Recall that types may not have any elements in Lean.
-It often happens that we would like a definition to return an arbitraryt element in a "corner case."
+It often happens that we would like a definition to return an arbitrary element in a "corner case."
 For example, we may like the expression ``head xs`` to be of type ``a`` when ``xs`` is of type ``List a``.
 Similarly, many theorems hold under the additional assumption that a type is not empty.
 For example, if ``a`` is a type, ``exists x : a, x = x`` is true only if ``a`` is not empty.

doc/typeobjs.md

@@ -114,7 +114,7 @@ constant α : Type _
 #check α
 ```
 
-Several Lean 3 users use the shorhand `Type*` for `Type _`. The `Type*` notation is not builtin in Lean 4, but you can easily define it using a `macro`.
+Several Lean 3 users use the shorthand `Type*` for `Type _`. The `Type*` notation is not builtin in Lean 4, but you can easily define it using a `macro`.
 ```lean
 macro "Type*" : term => `(Type _)
 

src/Lean/Elab/Inductive.lean

@@ -158,7 +158,7 @@ private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHead
 
 /- Create a local declaration for each inductive type in `rs`, and execute `x params indFVars`, where `params` are the inductive type parameters and
    `indFVars` are the new local declarations.
-   We use the the local context/instances and parameters of rs[0].
+   We use the local context/instances and parameters of rs[0].
    Note that this method is executed after we executed `checkHeaders` and established all
    parameters are compatible. -/
 private partial def withInductiveLocalDecls {α} (rs : Array ElabHeaderResult) (x : Array Expr → Array Expr → TermElabM α) : TermElabM α := do

src/Lean/Meta/ExprDefEq.lean

@@ -355,7 +355,7 @@ where
   addLetDeps : MetaM (Array Expr) := do
     let lctx ← getLCtx
     let s ← collectLetDeps
-    /- Convert `s` into the the array `ys` -/
+    /- Convert `s` into the array `ys` -/
     let start := lctx.getFVar! xs[0] |>.index
     let stop  := lctx.getFVar! xs.back |>.index
     let mut ys := #[]

src/Lean/Meta/WHNF.lean

@@ -393,7 +393,7 @@ mutual
 
   /--
     Auxiliary method for unfolding a class projection when transparency is set to `TransparencyMode.instances`.
-    Recall that that class instance projections are not marked with `[reducible]` because we want them to be
+    Recall that class instance projections are not marked with `[reducible]` because we want them to be
     in "reducible canonical form".
   -/
   private partial def unfoldProjInst (e : Expr) : MetaM (Option Expr) := do

src/Lean/MetavarContext.lean

@@ -41,7 +41,7 @@ first solution it finds. Consider the TC problem `Coe Nat ?x`,
 where `?x` is a metavariable created by the caller. There are many
 solutions to this problem (e.g., `?x := Int`, `?x := Real`, ...),
 and it doesn’t make sense to commit to the first one since TC does
-not know the the constraints the caller may impose on `?x` after the
+not know the constraints the caller may impose on `?x` after the
 TC problem is solved.
 Remark: we claim it is not feasible to make the whole system backtrackable,
 and allow the caller to backtrack back to TC and ask it for another solution

tests/bench/binarytrees.ghc-6.hs

@@ -40,7 +40,7 @@ main = do
     let vs = (depth minN maxN) `using` (parList $ evalTuple3 r0 r0 rseq)
     mapM_ (\((m,d,i)) -> io (show m ++ "\t trees") d i) vs
 
-    -- confirm the the long-lived binary tree still exists
+    -- confirm the long-lived binary tree still exists
     io "long lived tree" maxN (check long)
 
 -- generate many trees

tests/bench/binarytrees.lean

@@ -55,7 +55,7 @@ def main : List String → IO UInt32
   let vs := (depth minN maxN); -- `using` (parList $ evalTuple3 r0 r0 rseq)
   vs.forM (fun (m, d, i) => out (toString m ++ "\t trees") d i.get);
 
-  -- confirm the the long-lived binary tree still exists
+  -- confirm the long-lived binary tree still exists
   out "long lived tree" maxN (check long);
   pure 0
 | _ => pure 1