chore: fix typos, remove extra spaces (#121)

Co-authored-by: euprunin <[email protected]>
leanprover · Nov 1, 2024 · 2c73f5c · 2c73f5c
1 parent b6b502e
commit 2c73f5c
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 7 deletions.
diff --git a/Manual/BasicTypes/String/Logical.lean b/Manual/BasicTypes/String/Logical.lean
@@ -19,4 +19,4 @@ set_option pp.rawOnError true
 {docstring String}
 
 The logical model of strings in Lean is a structure that contains a single field, which is a list of characters.
-This is convenient when specifying and proving properties of string-processing fuctions at a low level.
+This is convenient when specifying and proving properties of string-processing functions at a low level.
diff --git a/Manual/Meta/Basic.lean b/Manual/Meta/Basic.lean
@@ -39,7 +39,7 @@ def runParserCategory (env : Environment) (opts : Lean.Options) (catName : Name)
     let p := andthenFn whitespace (categoryParserFnImpl catName)
     let ictx := mkInputContext input fileName
     let s := p.run ictx { env, options := opts } (getTokenTable env) (mkParserState input)
-    if !s.allErrors.isEmpty  then
+    if !s.allErrors.isEmpty then
       Except.error (toErrorMsg ictx s)
     else if ictx.input.atEnd s.pos then
       Except.ok s.stxStack.back
@@ -58,7 +58,7 @@ def runParser (env : Environment) (opts : Lean.Options) (p : Parser) (input : St
     let ictx := mkInputContext input fileName
     let p' := adaptCacheableContext ({· with prec}) p
     let s := p'.fn.run ictx { env, options := opts } (getTokenTable env) (mkParserState input)
-    if !s.allErrors.isEmpty  then
+    if !s.allErrors.isEmpty then
       Except.error (toErrorMsg ictx s)
     else if ictx.input.atEnd s.pos then
       Except.ok s.stxStack.back

diff --git a/Manual/Meta/Lean.lean b/Manual/Meta/Lean.lean
@@ -541,7 +541,7 @@ defmethod Lean.NameMap.getOrSuggest [Monad m] [MonadInfoTree m] [MonadError m]
   | none =>
     for (n, _) in map do
       -- TODO once Levenshtein is merged upstream, use it here
-      if FuzzyMatching.fuzzyMatch key.getId.toString n.toString || FuzzyMatching.fuzzyMatch n.toString key.getId.toString  then
+      if FuzzyMatching.fuzzyMatch key.getId.toString n.toString || FuzzyMatching.fuzzyMatch n.toString key.getId.toString then
         Suggestion.saveSuggestion key n.toString n.toString
     throwErrorAt key "'{key}' not found - options are {map.toList.map (·.fst)}"
 

diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean
@@ -111,7 +111,7 @@ intro n k
 ```
 ::::
 
-The {tactic}`case` and {tactic}`case'` tactics can be used to select a new main goal using the desired  goal's name.
+The {tactic}`case` and {tactic}`case'` tactics can be used to select a new main goal using the desired goal's name.
 When names are assigned in the context of a goal which itself has a name, the new goals's names are appended to the main goal's name with a dot (`'.', Unicode FULL STOP (0x2e)`) between them.
 
 ::::example "Hierarchical Goal Names"
@@ -789,7 +789,7 @@ When proving that {goal}`∀ (n : Nat), 0 + n = n`, the initial proof state is:
 ⊢ ∀ (n : Nat), 0 + n = n
 ```
 
-The tactic {tacticStep}`intro` results in a proof state with an inaccessible  assumption:
+The tactic {tacticStep}`intro` results in a proof state with an inaccessible assumption:
 
 ```post
 n✝ : Nat

diff --git a/Manual/Tactics/Conv.lean b/Manual/Tactics/Conv.lean
@@ -53,7 +53,7 @@ example (x y z : Nat) : x + (y + z) = (x + z) + y := by
 
 In this example, addition occurs under binders, so {tactic}`rw` can't be used.
 However, after using {tactic}`conv` to navigate to the function body, it succeeds.
-The nested use of {tactic}`conv` causes control to return to the current position in the term after performing further coversions on one of its subterms.
+The nested use of {tactic}`conv` causes control to return to the current position in the term after performing further conversions on one of its subterms.
 Because the goal is a reflexive equation after rewriting, {tactic}`conv` automatically closes it.
 
 ```lean