diff --git a/src/Lean/Compiler/LCNF/CoalesceRC.lean b/src/Lean/Compiler/LCNF/CoalesceRC.lean index e16da0baca..8e188d4ca4 100644 --- a/src/Lean/Compiler/LCNF/CoalesceRC.lean +++ b/src/Lean/Compiler/LCNF/CoalesceRC.lean @@ -21,7 +21,7 @@ Within a basic block, it is always safe to: until the later inc) and thus doing all relevant `inc` in the beginning doesn't change semantics. - Move all decrements on a variable to the last `dec` location (summing the counts). Because the - value is guaranteed to stay alive until at least the last `dec` anyway so a similiar argument to + value is guaranteed to stay alive until at least the last `dec` anyway so a similar argument to `inc` holds. Crucially this pass must be placed after `expandResetReuse` as that one relies on `inc`s still being diff --git a/src/Lean/Compiler/LCNF/ExpandResetReuse.lean b/src/Lean/Compiler/LCNF/ExpandResetReuse.lean index 22729f3125..c89f8f5e65 100644 --- a/src/Lean/Compiler/LCNF/ExpandResetReuse.lean +++ b/src/Lean/Compiler/LCNF/ExpandResetReuse.lean @@ -69,8 +69,8 @@ open ImpureType abbrev Mask := Array (Option FVarId) /-- -Try to erase `inc` instructions on projections of `targetId` occuring in the tail of `ds`. -Return the updated `ds` and mask contianing the `FVarId`s whose `inc` was removed. +Try to erase `inc` instructions on projections of `targetId` occurring in the tail of `ds`. +Return the updated `ds` and mask containing the `FVarId`s whose `inc` was removed. -/ partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (CodeDecl .impure)) : CompilerM (Array (CodeDecl .impure) × Mask) := do diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean index 57a476d8c9..311be55bbe 100644 --- a/src/Lean/Elab/Coinductive.lean +++ b/src/Lean/Elab/Coinductive.lean @@ -43,7 +43,7 @@ builtin_initialize Upon such rewrite, the code for adding flat inductives does not diverge much from the usual way its done for inductive declarations, but we omit applying attributes/modifiers and - we do not set the syntax references to track those declarations (as this is auxillary piece of + we do not set the syntax references to track those declarations (as this is auxiliary piece of data hidden from the user). Then, upon adding such flat inductives for each definition in the mutual block to the environment, @@ -345,7 +345,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do | throwError "expected to be quantifier" let motiveMVar ← mkFreshExprMVar type /- - We intro all the indices and the occurence of the coinductive predicate + We intro all the indices and the occurrence of the coinductive predicate -/ let (fvars, subgoal) ← motiveMVar.mvarId!.introN (info.numIndices + 1) subgoal.withContext do @@ -373,7 +373,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do -/ let originalCasesOn := mkAppN originalCasesOn indices /- - The next argument is the occurence of the coinductive predicate. + The next argument is the occurrence of the coinductive predicate. The original `casesOn` of the flat inductive mentions it in unrolled form, so we need to rewrite it. -/ @@ -447,7 +447,7 @@ public def elabCoinductive (coinductiveElabData : Array CoinductiveElabData) : T let consts := namesAndTypes.map fun (name, _) => (mkConst name levelParams) /- We create values of each of PreDefinitions, by taking existential (see `Meta.SumOfProducts`) - form of the associated flat inductives and applying paramaters, as well as recursive calls + form of the associated flat inductives and applying parameters, as well as recursive calls (with their parameters passed). -/ let preDefVals ← forallBoundedTelescope infos[0]!.type originalNumParams fun params _ => do diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean index fdfddeacf9..761b8324f7 100644 --- a/src/Lean/LibrarySuggestions/Basic.lean +++ b/src/Lean/LibrarySuggestions/Basic.lean @@ -91,10 +91,10 @@ end FoldRelevantConstantsImpl @[implemented_by FoldRelevantConstantsImpl.foldUnsafe] public opaque foldRelevantConstants {α : Type} (e : Expr) (init : α) (f : Name → α → MetaM α) : MetaM α := pure init -/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/ +/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/ public def relevantConstants (e : Expr) : MetaM (Array Name) := foldRelevantConstants e #[] (fun n ns => return ns.push n) -/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/ +/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/ public def relevantConstantsAsSet (e : Expr) : MetaM NameSet := foldRelevantConstants e ∅ (fun n ns => return ns.insert n) end Lean.Expr diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 5f643411f2..1ca46b5bb3 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -99,7 +99,7 @@ where if (← withReducibleAndInstances <| isDefEq x val) then return true else - trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign instance{indentExpr type}\nsythesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}" + trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign instance{indentExpr type}\nsynthesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}" return false | _ => trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}" diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean index 90eb9824a4..1d84c46700 100644 --- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean +++ b/src/Lean/Server/FileWorker/SemanticHighlighting.lean @@ -46,7 +46,7 @@ structure LeanSemanticToken where stx : Syntax /-- Type of the semantic token. -/ type : SemanticTokenType - /-- In case of overlap, higher-priority tokens will take precendence -/ + /-- In case of overlap, higher-priority tokens will take precedence -/ priority : Nat := 5 /-- Semantic token information with absolute LSP positions. -/ @@ -57,7 +57,7 @@ structure AbsoluteLspSemanticToken where tailPos : Lsp.Position /-- Start position of the semantic token. -/ type : SemanticTokenType - /-- In case of overlap, higher-priority tokens will take precendence -/ + /-- In case of overlap, higher-priority tokens will take precedence -/ priority : Nat := 5 deriving BEq, Hashable, FromJson, ToJson diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index 474be93891..aa96ac1b5f 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -386,7 +386,7 @@ OPTIONS: --force-download redownload existing files Downloads build outputs for packages in the workspace from a remote cache -service. The cache service used can be specifed via the `--service` option. +service. The cache service used can be specified via the `--service` option. Otherwise, Lake will the system default, or, if none is configured, Reservoir. See `lake cache services` for more information on how to configure services. @@ -429,7 +429,7 @@ USAGE: Uploads the input-to-output mappings contained in the specified file along with the corresponding output artifacts to a remote cache. The cache service -used via be specified via `--service` option. If not specifed, Lake will used +used can be specified via the `--service` option. If not specified, Lake will use the system default, or error if none is configured. See the help page of `lake cache services` for more information on how to configure services. diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index d2523fc48a..65b0e7fd0d 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -446,7 +446,7 @@ protected def get : CliM PUnit := do logWarning endpointDeprecation if opts.mappingsOnly then error "`--mappings-only` requires services to be configured - via the Lake system configuration (not enviroment variables)" + via the Lake system configuration (not environment variables)" return .downloadService artifactEndpoint revisionEndpoint ws.lakeEnv.cacheService? | none, none => return ws.defaultCacheService