diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean index 2cec66e95317..be40d12c4e9b 100644 --- a/src/Lean/Compiler/InlineAttrs.lean +++ b/src/Lean/Compiler/InlineAttrs.lean @@ -40,7 +40,7 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do declName' == ``WellFounded.Nat.fix || declName' == declName ++ `_unary -- Auxiliary declaration created by `WF` module if Option.isSome <| info.value.find? fun e => e.isConst && isRec e.constName! then - -- It contains a `brecOn` or `WellFounded.fix` application. So, it should be recursvie + -- It contains a `brecOn` or `WellFounded.fix` application. So, it should be recursive return false return true diff --git a/src/Lean/Compiler/LCNF/JoinPoints.lean b/src/Lean/Compiler/LCNF/JoinPoints.lean index 4d2981a40a62..2716f0e4146f 100644 --- a/src/Lean/Compiler/LCNF/JoinPoints.lean +++ b/src/Lean/Compiler/LCNF/JoinPoints.lean @@ -287,7 +287,7 @@ abbrev ExtendM := ReaderT ExtendContext StateRefT ExtendState ScopeM Replace a free variable if necessary, that is: - It is in the list of candidates - We are currently within a join point (if we are within a function there - cannot be a need to replace them since we dont extend their context) + cannot be a need to replace them since we don't extend their context) - Said join point actually has a replacement parameter registered. otherwise just return `fvar`. -/ diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean index 502040c55a06..8ff85d9a9cd2 100644 --- a/src/Lean/Compiler/LCNF/Specialize.lean +++ b/src/Lean/Compiler/LCNF/Specialize.lean @@ -226,7 +226,7 @@ def shouldSpecialize (specEntry : SpecEntry) (args : Array Arg) : SpecializeM Bo If we have `f p` where `p` is a param it makes no sense to specialize as we will just close over `p` again and will have made no progress. - The reason for doing this only for declarations which have have already been specialised + The reason for doing this only for declarations which have already been specialised themselves is, that we *must* always specialize declarations that are marked with `@[specialize]`. This is because the specializer will not specialize their bodies because it waits for the bodies to be specialized at the call site. This is for example important in diff --git a/src/Lean/Compiler/LCNF/ToDecl.lean b/src/Lean/Compiler/LCNF/ToDecl.lean index 9805f0b319d4..3ff4e694c66c 100644 --- a/src/Lean/Compiler/LCNF/ToDecl.lean +++ b/src/Lean/Compiler/LCNF/ToDecl.lean @@ -92,7 +92,7 @@ def declIsNotUnsafe (declName : Name) : CoreM Bool := do return false else if info matches .opaqueInfo .. then - -- check if its a partial def + -- check if it's a partial def return env.find? (Compiler.mkUnsafeRecName declName) |>.isNone else return true diff --git a/src/Lean/DefEqAttrib.lean b/src/Lean/DefEqAttrib.lean index f61e6a78921d..5ae02ba77bc7 100644 --- a/src/Lean/DefEqAttrib.lean +++ b/src/Lean/DefEqAttrib.lean @@ -56,7 +56,7 @@ Marks the theorem as a definitional equality. The theorem must be an equality that holds by `rfl`. This allows `dsimp` to use this theorem when rewriting. -A theorem with with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`. +A theorem with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`. To avoid this behavior, write `:= (rfl)` instead. The attribute should be given before a `@[simp]` attribute to have effect. diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean index 57a476d8c9cb..d935c38454cd 100644 --- a/src/Lean/Elab/Coinductive.lean +++ b/src/Lean/Elab/Coinductive.lean @@ -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/Elab/Do/Legacy.lean b/src/Lean/Elab/Do/Legacy.lean index 0241bed712f5..603f7e1c771e 100644 --- a/src/Lean/Elab/Do/Legacy.lean +++ b/src/Lean/Elab/Do/Legacy.lean @@ -201,7 +201,7 @@ def AltExpr.vars (alt : AltExpr σ) : Array Var := Id.run do `vars` is the array of variables declared by it, and `cont` is the next instruction in the `do` code block. `vars` is an array since we have declarations such as `let (a, b) := s`. - - `reassign` is an reassignment-like `doElem` (e.g., `x := x + 1`). + - `reassign` is a reassignment-like `doElem` (e.g., `x := x + 1`). - `joinpoint` is a join point declaration: an auxiliary `let`-declaration used to represent the control-flow. diff --git a/src/Lean/Elab/PreDefinition/FixedParams.lean b/src/Lean/Elab/PreDefinition/FixedParams.lean index 01fd9b600987..6cd210b6359d 100644 --- a/src/Lean/Elab/PreDefinition/FixedParams.lean +++ b/src/Lean/Elab/PreDefinition/FixedParams.lean @@ -462,7 +462,7 @@ def FixedParamPerms.erase (fixedParamPerms : FixedParamPerms) (xs : Array Expr) assert! paramIdx < mapping.size if let some fixedParamIdx := mapping[paramIdx]! then mask := mask.set! fixedParamIdx true - -- Take the transitive closure under under `fixedParamPerms.revDeps`. + -- Take the transitive closure under `fixedParamPerms.revDeps`. let mut changed := true while changed do changed := false diff --git a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean index 3b20ebffd4a3..02bd36f6069a 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean @@ -15,7 +15,7 @@ This module contains the types * `IndGroupInfo`, a variant of `InductiveVal` with information that applies to a whole group of mutual inductives and * `IndGroupInst` which extends `IndGroupInfo` with levels and parameters - to indicate a instantiation of the group. + to indicate an instantiation of the group. One purpose of this abstraction is to make it clear when a function operates on a group as a whole, rather than a specific inductive within the group. @@ -50,7 +50,7 @@ partial def IndGroupInfo.brecOnName (info : IndGroupInfo) (idx : Nat) : Name := info.brecOnName 0 |>.appendIndexAfter j /-- -An instance of an mutually inductive group of inductives, identified by the `all` array +An instance of a mutually inductive group of inductives, identified by the `all` array and the level and expressions parameters. For example this distinguishes between `List α` and `List β` so that we will not even attempt diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 9379c90e1765..56f10c0892ae 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -54,7 +54,7 @@ This is a hack to fix fallout from #8519, where a non-exposed wfrec definition ` in a module would cause `foo.eq_def` to be defined eagerly and privately, but it should still be visible from non-module files. -So we create a unfold equation generator that aliases an existing private `eq_def` to +So we create an unfold equation generator that aliases an existing private `eq_def` to wherever the current module expects it. -/ def copyPrivateUnfoldTheorem : GetUnfoldEqnFn := fun declName => do diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index e65d855080cc..d3303e8879be 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -2138,7 +2138,7 @@ sufficient for our purposes. We may have to revise this design decision and eagerly generate equational theorems when we implement the module system. -Remark: we do not check whether the theorem `value` field match. This feature is useful and +Remark: we do not check whether the theorem `value` field matches. This feature is useful and ensures the proofs for equational theorems do not need to be identical. This decision relies on the fact that theorem types are propositions, we have proof irrelevance, and theorems are (mostly) opaque in Lean. For `Acc.rec`, we may unfold theorems diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean index ba8f1820e685..5f43d1f97ea9 100644 --- a/src/Lean/LibrarySuggestions/Basic.lean +++ b/src/Lean/LibrarySuggestions/Basic.lean @@ -92,10 +92,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/LocalContext.lean b/src/Lean/LocalContext.lean index 206380f65754..1f42146f6e36 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -598,7 +598,7 @@ def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) (usedLetOnly : B @[inline] def all (lctx : LocalContext) (p : LocalDecl → Bool) : Bool := Id.run <| lctx.allM (pure <| p ·) -/-- If option `pp.sanitizeNames` is set to `true`, add tombstone to shadowed local declaration names and ones contains macroscopes. -/ +/-- If option `pp.sanitizeNames` is set to `true`, add tombstone to shadowed local declaration names and ones containing macroscopes. -/ def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext := do let st ← get if !getSanitizeNames st.options then pure lctx else diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 1b824ef014ef..411b7405b6e8 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -22,9 +22,9 @@ import Lean.Meta.Match.NamedPatterns /-! This module implements the backend of match compilation. The elaborator has already elaborated -the patterns and the the expected type of the matcher is known. +the patterns and the expected type of the matcher is known. -The match compilation task is represented as a `Problem`, which is then processed interatively by +The match compilation task is represented as a `Problem`, which is then processed iteratively by the `process` function. It has various “moves” which it tries in a particular order, to make progress on the problem, possibly splitting it. diff --git a/src/Lean/Meta/PProdN.lean b/src/Lean/Meta/PProdN.lean index fb85f25fc8ab..d2dbe30bb085 100644 --- a/src/Lean/Meta/PProdN.lean +++ b/src/Lean/Meta/PProdN.lean @@ -150,7 +150,7 @@ def projM (n i : Nat) (e : Expr) : MetaM Expr := do /-- Packs multiple type-forming lambda expressions taking the same parameters using `PProd`. -The parameter `type` is the common type of the these expressions +The parameter `type` is the common type of these expressions For example ``` diff --git a/src/Lean/Meta/Sym/Pattern.lean b/src/Lean/Meta/Sym/Pattern.lean index 964a4cc419da..2aa31cb427ca 100644 --- a/src/Lean/Meta/Sym/Pattern.lean +++ b/src/Lean/Meta/Sym/Pattern.lean @@ -213,7 +213,7 @@ partial def process (p : Expr) (e : Expr) : UnifyM Bool := do /- **Note**: Most patterns do not have free variables since they are created from top-level theorems. That said, some user may want to create patterns using local hypotheses, and they - may contain free variables. This is not the common case. So, we just push to pending an continue. + may contain free variables. This is not the common case. So, we just push to pending and continue. -/ pushPending p e return true diff --git a/src/Lean/Meta/Tactic/Grind/AC/Types.lean b/src/Lean/Meta/Tactic/Grind/AC/Types.lean index 2e55d27af698..082385caf731 100644 --- a/src/Lean/Meta/Tactic/Grind/AC/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/AC/Types.lean @@ -117,7 +117,7 @@ structure State where -/ structs : Array Struct := {} /-- - Mapping from operators to its "operator id". We cache failures using `none`. + Mapping from operators to their "operator id". We cache failures using `none`. `opIdOf[op]` is `some id`, then `id < structs.size`. -/ opIdOf : PHashMap ExprPtr (Option Nat) := {} /-- diff --git a/src/Lean/Meta/Tactic/Grind/Order/Types.lean b/src/Lean/Meta/Tactic/Grind/Order/Types.lean index 5608094943fd..c6ed91d5232d 100644 --- a/src/Lean/Meta/Tactic/Grind/Order/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Order/Types.lean @@ -134,7 +134,7 @@ structure State where /-- Order structures detected. -/ structs : Array Struct := {} /-- - Mapping from types to its "structure id". We cache failures using `none`. + Mapping from types to their "structure id". We cache failures using `none`. `typeIdOf[type]` is `some id`, then `id < structs.size`. -/ typeIdOf : PHashMap ExprPtr (Option Nat) := {} /-- Mapping from expressions/terms to their structure ids. -/ diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index fad4a4831c62..540982305867 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -295,7 +295,7 @@ def withSplitSource [MonadControlT GrindM m] [Monad m] (splitSource : SplitSourc def getConfig : GrindM Grind.Config := return (← readThe Context).config -/-- Returns extension states associate with `grind` attributes in use -/ +/-- Returns extension states associated with `grind` attributes in use -/ def getExtensions : GrindM Grind.ExtensionStateArray := return (← readThe Context).extensions @@ -1211,7 +1211,7 @@ def isEqv (a b : Expr) : GoalM Bool := do let some nb ← getENode? b | return false return isSameExpr na.root nb.root -/-- Returns `true` if the root of its equivalence class. -/ +/-- Returns `true` if `e` is the root of its equivalence class. -/ def isRoot (e : Expr) : GoalM Bool := do let some n ← getENode? e | return false -- `e` has not been internalized. Panic instead? return isSameExpr n.root e @@ -1242,7 +1242,7 @@ def getRootENode? (e : Expr) : GoalM (Option ENode) := do let some n ← getENode? e | return none getENode? n.root /-- -Returns `true` if the ENode associate with `e` has support for function equality +Returns `true` if the ENode associated with `e` has support for function equality congruence closure. See `Grind.Config.funCC` for additional details. -/ def useFunCC (e : Expr) : GoalM Bool := @@ -1419,7 +1419,7 @@ For each equality `b = c` in `parents`, executes `k b c` IF else k b c -/-- Returns `true` is `e` is the root of its congruence class. -/ +/-- Returns `true` if `e` is the root of its congruence class. -/ def isCongrRoot (e : Expr) : GoalM Bool := do return (← getENode e).isCongrRoot diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 809fbcc0b4ec..6e1d58fd1355 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -210,7 +210,7 @@ private def isWFRec (declName : Name) : Bool := /-- Helper method for `reduceRec`. We use it to ensure we don't expose `Nat.add` when reducing `Nat.rec`. -We we use the following trick, if `e` can be expressed as an offset `(a, k)` with `k > 0`, +We use the following trick: if `e` can be expressed as an offset `(a, k)` with `k > 0`, we create a new expression `Nat.succ e'` where `e'` is `a` for `k = 1`, or `a + (k-1)` for `k > 1`. See issue #3022 -/ diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 5b38ff62d808..b7fe63dd7ae8 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -151,7 +151,7 @@ def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s => /-- Generate an error at the position saved with the `withPosition` combinator. If `delta == true`, then it reports at saved position+1. - This useful to make sure a parser consumed at least one character. -/ + This is useful to make sure a parser consumed at least one character. -/ @[builtin_doc] def errorAtSavedPos (msg : String) (delta : Bool) : Parser := { fn := errorAtSavedPosFn msg delta } diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index ae00cacc434b..f37acb6b3a65 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -884,7 +884,7 @@ binder group `(d e ...)` as determined by `shouldGroupWithNext`. We cannot do gr inside-out, on the Syntax level, because it depends on comparing the Expr binder types. The `allNames` set is used to make sure names in the same `fun` binders are unique. -Users have reported than `fun x x x => x` is confusing. +Users have reported that `fun x x x => x` is confusing. -/ private partial def delabBinders (allNames : NameSet) (curNames : Array Syntax) (dep ppTypes : Bool) (delabBody : NameSet → Delab) diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 228d6e1d3a9a..f278f9cb7c2c 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -33,7 +33,7 @@ def findCompletionCmdDataAtPos : ServerTask (Option (Syntax × Elab.InfoTree)) := -- `findCmdDataAtPos` may produce an incorrect snapshot when `pos` is in whitespace. -- However, most completions don't need trailing whitespace at the term level; - -- synthetic completions are the only notions of completion that care care about whitespace. + -- synthetic completions are the only notions of completion that care about whitespace. -- Synthetic tactic completion only needs the `ContextInfo` of the command, so any snapshot -- will do. -- Synthetic field completion in `{ }` doesn't care about whitespace; diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean index e39a8b9f94ec..440045669f29 100644 --- a/src/Lean/Shell.lean +++ b/src/Lean/Shell.lean @@ -108,7 +108,7 @@ opaque Internal.enableDebug (tag : @& String) : BaseIO Unit /-- Lean's short version string (i.e., what is printed by `lean --short-version`). -This is the Lean equivalent of of the C++ `LEAN_VERSION_STRING` / `g_short_version_string`. +This is the Lean equivalent of the C++ `LEAN_VERSION_STRING` / `g_short_version_string`. -/ def shortVersionString : String := if version.specialDesc ≠ "" then diff --git a/src/runtime/libuv.h b/src/runtime/libuv.h index 87fbcabc3049..160a7d5d7c07 100644 --- a/src/runtime/libuv.h +++ b/src/runtime/libuv.h @@ -18,7 +18,6 @@ Author: Markus Himmel, Sofia Rodrigues #include "runtime/object.h" #include "runtime/thread.h" #include "runtime/allocprof.h" -#include "runtime/object.h" namespace lean { diff --git a/src/runtime/object_ref.h b/src/runtime/object_ref.h index 6b712ff4d660..e7fb1be02d83 100644 --- a/src/runtime/object_ref.h +++ b/src/runtime/object_ref.h @@ -206,7 +206,7 @@ inline object * mk_except_error_string(char const * err) { return r; } -/* Given `o` representing a Lean value of type `Except String A`, return `T` an smart pointer +/* Given `o` representing a Lean value of type `Except String A`, return `T` a smart pointer that encapsulates `A` values or throw an exception */ template T get_except_value(obj_arg o) { if (cnstr_tag(o) == 1) {