From 2c73f5c7f556b89027248f8fa7ec30b0c5f793ff Mon Sep 17 00:00:00 2001 From: euprunin Date: Fri, 1 Nov 2024 22:36:18 +0100 Subject: [PATCH] chore: fix typos, remove extra spaces (#121) Co-authored-by: euprunin --- Manual/BasicTypes/String/Logical.lean | 2 +- Manual/Meta/Basic.lean | 4 ++-- Manual/Meta/Lean.lean | 2 +- Manual/Tactics.lean | 4 ++-- Manual/Tactics/Conv.lean | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Manual/BasicTypes/String/Logical.lean b/Manual/BasicTypes/String/Logical.lean index 1bce7f2..ae1764f 100644 --- 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 index b3c859a..30771c3 100644 --- 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 index bae7163..cb7ff8d 100644 --- 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 index e8b52c0..0e57bc4 100644 --- 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 index 4b001e6..2973c3a 100644 --- 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