From 2ca3bc28590c5c33f755d3bd18252f25ea266266 Mon Sep 17 00:00:00 2001 From: Tom Levy Date: Sun, 7 Dec 2025 02:54:27 +1300 Subject: [PATCH] chore: fix spelling (#11531) Hi, these are just some spelling corrections. There is one I wasn't completely sure about in src/Init/Data/List/Lemmas.lean: > See also > ... > Also > \* \`Init.Data.List.Monadic\` for **addiation** _(additional?)_ lemmas about \`List.mapM\` and \`List.forM\` --- src/Init/Data/BitVec/Bitblast.lean | 2 +- src/Init/Data/BitVec/Lemmas.lean | 2 +- src/Init/Data/Bool.lean | 2 +- src/Init/Data/List/Basic.lean | 2 +- src/Init/Data/List/Lemmas.lean | 2 +- src/Init/Data/List/Sublist.lean | 2 +- src/Init/Data/String/Basic.lean | 2 +- src/Init/Data/String/Decode.lean | 2 +- src/Init/Data/UInt/Basic.lean | 2 +- src/Init/System/IO.lean | 2 +- src/Init/Tactics.lean | 2 +- src/Lean/Attributes.lean | 2 +- src/Lean/Compiler/IR/LiveVars.lean | 2 +- src/Lean/Elab/Coinductive.lean | 6 +++--- src/Lean/Elab/DocString.lean | 2 +- src/Lean/Elab/DocString/Builtin.lean | 6 +++--- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/MutualInductive.lean | 2 +- src/Lean/Elab/PreDefinition/FixedParams.lean | 2 +- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 2 +- src/Lean/Elab/PreDefinition/WF/Preprocess.lean | 2 +- src/Lean/Elab/StructInst.lean | 2 +- src/Lean/Elab/Tactic/Induction.lean | 4 ++-- src/Lean/Elab/Tactic/Try.lean | 2 +- src/Lean/Environment.lean | 2 +- src/Lean/ErrorExplanations/InvalidField.lean | 2 +- src/Lean/Meta/Basic.lean | 2 +- src/Lean/Meta/CasesInfo.lean | 2 +- src/Lean/Meta/Constructions/CasesOnSameCtor.lean | 4 ++-- src/Lean/Meta/Constructions/CtorElim.lean | 2 +- src/Lean/Meta/Constructions/SparseCasesOn.lean | 2 +- src/Lean/Meta/Eqns.lean | 2 +- src/Lean/Meta/ExprDefEq.lean | 2 +- src/Lean/Meta/IndPredBelow.lean | 2 +- src/Lean/Meta/Match/AltTelescopes.lean | 4 ++-- src/Lean/Meta/Match/MatcherInfo.lean | 6 +++--- src/Lean/Meta/Tactic/FunInd.lean | 2 +- src/Lean/Meta/Tactic/Grind/Internalize.lean | 2 +- src/Lean/Meta/Tactic/Simp/Main.lean | 2 +- src/Lean/Meta/Tactic/Simp/RegisterCommand.lean | 2 +- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 4 ++-- src/Lean/Meta/Tactic/Split.lean | 2 +- src/Lean/Meta/Tactic/UnifyEq.lean | 2 +- src/Lean/Meta/Transform.lean | 2 +- src/Lean/Util/Trace.lean | 2 +- src/Std/Data/DTreeMap/Raw/Basic.lean | 4 ++-- .../BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean | 2 +- src/lake/Lake/Build/Context.lean | 2 +- src/lake/Lake/Build/Target/Fetch.lean | 2 +- src/lake/Lake/Config/ConfigDecl.lean | 4 ++-- src/lake/Lake/Config/InputFileConfig.lean | 2 +- src/lake/Lake/Config/Workspace.lean | 2 +- tests/lean/grind/experiments/bitvec.lean | 2 +- tests/lean/run/grind_bitvec2.lean | 2 +- tests/lean/run/grind_qsort.lean | 4 ++-- tests/lean/run/issue8939wf.lean | 2 +- tests/lean/run/timeParse.lean | 2 +- 57 files changed, 70 insertions(+), 70 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 2465eb8c3b..55ff9deae6 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -835,7 +835,7 @@ execution. -/ structure DivModArgs (w : Nat) where /-- the numerator (aka, dividend) -/ n : BitVec w - /-- the denumerator (aka, divisor)-/ + /-- the denominator (aka, divisor)-/ d : BitVec w /-- A `DivModState` is lawful if the remainder width `wr` plus the numerator width `wn` equals `w`, diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 3f39df519e..4ba294b9cb 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -5601,7 +5601,7 @@ theorem msb_eq_toNat {x : BitVec w}: simp only [msb_eq_decide, ge_iff_le] /-- Negating a bitvector created from a natural number equals -creating a bitvector from the the negative of that number. +creating a bitvector from the negative of that number. -/ theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} : - BitVec.ofNat w x = BitVec.ofInt w (- x) := by diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index 862d65879f..5daaa2d23d 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -260,7 +260,7 @@ instance : Std.Associative (· != ·) := ⟨bne_assoc⟩ theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y := by decide -/-! ### coercision related normal forms -/ +/-! ### coercion related normal forms -/ theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) : (a == b) = decide (a = b) := by diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index f0505abdfd..a13b64d17e 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -2252,7 +2252,7 @@ def eraseReps {α} [BEq α] (as : List α) : List α := eraseRepsBy (· == ·) a /-! ### span -/ /-- -Splits a list into the the longest initial segment for which `p` returns `true`, paired with the +Splits a list into the longest initial segment for which `p` returns `true`, paired with the remainder of the list. `O(|l|)`. diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 7735f1c125..a492a8330a 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -77,7 +77,7 @@ Further results, which first require developing further automation around `Nat`, * `Init.Data.List.Nat.TakeDrop`: `List.take` and `List.drop` Also -* `Init.Data.List.Monadic` for addiation lemmas about `List.mapM` and `List.forM`. +* `Init.Data.List.Monadic` for additional lemmas about `List.mapM` and `List.forM`. -/ diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 8c60f45396..2ee3e38399 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -249,7 +249,7 @@ theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _) | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)] --- Only activative `eq_of_length` if we're already thinking about lengths. +-- Only activate `eq_of_length` if we're already thinking about lengths. grind_pattern Sublist.eq_of_length => l₁ <+ l₂, length l₁, length l₂ theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ := diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 97b8ce2629..be1f740fb5 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1177,7 +1177,7 @@ position. -/ def Slice.Pos.get? {s : Slice} (pos : s.Pos) : Option Char := if h : pos = s.endPos then none else some (pos.get h) -/-- Returns the byte at the given position in the string, or panicks if the position is the end +/-- Returns the byte at the given position in the string, or panics if the position is the end position. -/ @[expose] def Slice.Pos.get! {s : Slice} (pos : s.Pos) : Char := diff --git a/src/Init/Data/String/Decode.lean b/src/Init/Data/String/Decode.lean index 98dfa5aa6b..e756355861 100644 --- a/src/Init/Data/String/Decode.lean +++ b/src/Init/Data/String/Decode.lean @@ -529,7 +529,7 @@ public def assemble₂ (w x : UInt8) : Option Char := else let r := assemble₂Unchecked w x if r < 0x80 then - none -- overlong encodinlg + none -- overlong encoding else some ⟨r, ?onemore⟩ where finally diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean index 872fe72d6e..2d2b0c7ce1 100644 --- a/src/Init/Data/UInt/Basic.lean +++ b/src/Init/Data/UInt/Basic.lean @@ -517,7 +517,7 @@ protected def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (UI Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the `<` operator. -/ --- These need to be exposed as `Init.Prelude` already has an instance for bootstrapping puproses and +-- These need to be exposed as `Init.Prelude` already has an instance for bootstrapping purposes and -- they should be defeq @[expose] protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec /-- diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 3d7b37f7e2..6d6b1ddb83 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -837,7 +837,7 @@ Encountering an EOF does not close a handle. Subsequent reads may block and retu -/ @[extern "lean_io_prim_handle_read"] opaque read (h : @& Handle) (bytes : USize) : IO ByteArray /-- -Writes the provided bytes to the the handle. +Writes the provided bytes to the handle. Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use `IO.FS.Handle.flush` to write changes to buffers to the associated device. diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 8fa4c6f8f3..8d14f93813 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -1004,7 +1004,7 @@ You can use `with` to provide the variables names for each constructor. syntax (name := cases) "cases " elimTarget,+ (" using " term)? (inductionAlts)? : tactic /-- -The `fun_induction` tactic is a convenience wrapper around the `induction` tactic to use the the +The `fun_induction` tactic is a convenience wrapper around the `induction` tactic to use the functional induction principle. The tactic invocation diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 3c349e53d3..535ea787e0 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -250,7 +250,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where afterSet : Name → α → AttrM Unit := fun _ _ _ => pure () /-- If set, entries are not resorted on export and `getParam?` will fall back to a linear instead of - binary search insde an imported module's entries. + binary search inside an imported module's entries. -/ preserveOrder : Bool := false /-- diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean index 10a25e5911..c0bbfc5ba5 100644 --- a/src/Lean/Compiler/IR/LiveVars.lean +++ b/src/Lean/Compiler/IR/LiveVars.lean @@ -68,7 +68,7 @@ partial def visitFnBody (w : Index) : FnBody → M Bool -- Instead of marking the join points that we have already been visited, we permanently remove `j` from the context. set (ctx.eraseJoinPointDecl j) *> visitFnBody w b | none => - -- `j` must be a local join point. So do nothing since we have already visite its body. + -- `j` must be a local join point. So do nothing since we have already visited its body. pure false | .ret x => visitArg w x diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean index d93edf1f8e..57a476d8c9 100644 --- a/src/Lean/Elab/Coinductive.lean +++ b/src/Lean/Elab/Coinductive.lean @@ -72,7 +72,7 @@ builtin_initialize Note that at this point `PartialFixpoint` machinery applies the attributes and modifiers. We use the syntax references from the original `InductiveView`s and set them to those declarations. - Moreover, we have following theorem (generated by `generateEqLemmas`) that connets the coinductive + Moreover, we have following theorem (generated by `generateEqLemmas`) that connects the coinductive predicate to its flat inductive: ``` info: infSeq.functor_unfold (α : Type) (r : α → α → Prop) (a✝ : α) : infSeq α r a✝ = infSeq._functor α r (infSeq α r) a✝ @@ -250,7 +250,7 @@ private def generateCoinductiveConstructor (infos : Array InductiveVal) (ctorSyn let newHole ← hole.replaceTargetEq rewriteResult.eNew rewriteResult.eqProof /- - Now, all it suffices is to call an approprate constructor of the flat inductive. + Now, all it suffices is to call an appropriate constructor of the flat inductive. -/ let constructor := mkConst ctor.name levelParams let constructor := mkAppN constructor params @@ -365,7 +365,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do -- Then we apply the metavariable to the `casesOn` of the flat inductive let originalCasesOn := mkApp originalCasesOn motiveMVar - -- The next arguemnts of the `casesOn` are type indices + -- The next arguments of the `casesOn` are type indices forallBoundedTelescope goalType info.numIndices fun indices goalType => do /- The types do not change, so we just make free variables for them diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean index eb3dc23c53..0ca292a482 100644 --- a/src/Lean/Elab/DocString.lean +++ b/src/Lean/Elab/DocString.lean @@ -278,7 +278,7 @@ where ids.getArgs.mapM fun x => if x.getKind == identKind || x.getKind == ``hole then pure (some x) - else throwErrorAt x "identifer or `_` expected" + else throwErrorAt x "identifier or `_` expected" set_option linter.unusedVariables false in diff --git a/src/Lean/Elab/DocString/Builtin.lean b/src/Lean/Elab/DocString/Builtin.lean index 71ba171c0e..0f750ab02d 100644 --- a/src/Lean/Elab/DocString/Builtin.lean +++ b/src/Lean/Elab/DocString/Builtin.lean @@ -884,7 +884,7 @@ deriving TypeName /-- Elaborates a sequence of Lean commands as examples. -To make examples self-contained, elaboration ignores the surrouncing section scopes. Modifications +To make examples self-contained, elaboration ignores the surrounding section scopes. Modifications to the environment are preserved during a single documentation comment, and discarded afterwards. The named argument `name` allows a name to be assigned to the code block; any messages created by @@ -1271,7 +1271,7 @@ def «set_option» (option : Ident) (value : DataValue) : DocM (Block ElabInline return .empty /-- -Constructs a link to the Lean langauge reference. Two positional arguments are expected: +Constructs a link to the Lean language reference. Two positional arguments are expected: * `domain` should be one of the valid domains, such as `section`. * `name` should be the content's canonical name in the domain. -/ @@ -1468,7 +1468,7 @@ def suggestSyntax (code : StrLit) : DocM (Array CodeSuggestion) := do for (catName, _) in cats do try let stx ← parseStrLit (whitespace >> (categoryParser catName 0).fn) code - -- Many syntax categories admit identifers, so the false postitive rate is high + -- Many syntax categories admit identifiers, so the false positive rate is high unless onlyIdent stx do candidates := candidates.push catName catch | _ => pure () diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 99d6e44dfb..97a7e98b62 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -217,7 +217,7 @@ def Vec.map' (f : α → β) (xs : Vec α n) : Vec β n := We had to include `n` and the `_`s because the type of `xs` depends on `n`. Moreover, `nil` and `cons a as` have different types. This was quite tedious. So, we have implemented an automatic "discriminant refinement procedure". -The procedure is based on the observation that we get a type error whenenver we forget to include `_`s +The procedure is based on the observation that we get a type error whenever we forget to include `_`s and the indices a discriminant depends on. So, we catch the exception, check whether the type of the discriminant is an indexed family, and add their indices as new discriminants. diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index acffab1b27..50208ff64a 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -959,7 +959,7 @@ private def mkFlatInductive (views : Array InductiveView) forallBoundedTelescope indType numParams fun indTypeParams indTypeBody => do -- We first go through all types in the mutual block and get rid of their parameters - -- by substiuting free variables + -- by substituting free variables let typesWithAppliedParams ← namesAndTypes.mapM fun (newName, curIndType) => do forallBoundedTelescope curIndType numParams fun curIntTypeParams curIndTypeBody => do return (newName, curIndTypeBody.replaceFVars curIntTypeParams indTypeParams) diff --git a/src/Lean/Elab/PreDefinition/FixedParams.lean b/src/Lean/Elab/PreDefinition/FixedParams.lean index 514b11e1c7..01fd9b6009 100644 --- a/src/Lean/Elab/PreDefinition/FixedParams.lean +++ b/src/Lean/Elab/PreDefinition/FixedParams.lean @@ -307,7 +307,7 @@ def FixedParamPerm.isFixed (perm : FixedParamPerm) (i : Nat) : Bool := perm[i]?.join.isSome /-- -Brings the fixed parameters from `type`, which should the the type of the `funIdx`'s function, into +Brings the fixed parameters from `type`, which should be the type of the `funIdx`'s function, into scope. -/ private partial def FixedParamPerm.forallTelescopeImpl (perm : FixedParamPerm) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 4ae676d3bf..d1266ff0c9 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -807,7 +807,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) let recCalls := filterSubsumed recCalls -- For every function, the measures we want to use - -- (One for each non-forbiddend arg) + -- (One for each non-forbidden arg) let basicMeasures₁ ← simpleMeasures preDefs fixedParamPerms userVarNamess let basicMeasures₂ ← complexMeasures preDefs fixedParamPerms userVarNamess recCalls let basicMeasures := Array.zipWith (· ++ ·) basicMeasures₁ basicMeasures₂ diff --git a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean index 1b6b2a2e22..991ad75441 100644 --- a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean +++ b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean @@ -48,7 +48,7 @@ The process proceeds in these steps, to guide the transformation: The `binderNameHint` preserves the user-chosen name in `f` if that is a lambda. - The `wfParam` on the right hand side ensurses that doubly-nested recursion works. + The `wfParam` on the right hand side ensures that doubly-nested recursion works. 4. All left-over `wfParam` gadgets are removed. diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 1e855cad39..73f980fa24 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -804,7 +804,7 @@ private def synthOptParamFields : StructInstM Unit := do /- We must use `checkedAssign` here to ensure we do not create a cyclic assignment. See #3150. - This can happen when there are holes in the the fields the default value + This can happen when there are holes in the fields the default value depends on. Possible improvement: create a new `_` instead of returning `false` when `checkedAssign` fails. Reason: the field will not be needed after the diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 4273c2a8e9..11debd2bf6 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -49,7 +49,7 @@ def getAltName? (alt : Syntax) : Option Name := else let ident := head[1] if ident.isOfKind identKind then some ident.getId.eraseMacroScopes else none -/-- Returns true if the the alternative is for a wildcard, and that the wildcard is not due to a syntax error. -/ +/-- Returns true if the alternative is for a wildcard, and that the wildcard is not due to a syntax error. -/ def isAltWildcard (altStx : Syntax) : Bool := getAltName? altStx == some `_ /-- Returns the `inductionAlt` `ident <|> hole` -/ @@ -233,7 +233,7 @@ public partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : /-- Given a goal `... targets ... |- C[targets, complexArgs]` associated with `mvarId`, -where `complexArgs` are the the complex (i.e. non-target) arguments to the motive in the conclusion +where `complexArgs` are the complex (i.e. non-target) arguments to the motive in the conclusion of the eliminator, construct `motiveArg := fun targets rs => C[targets, rs]` This checks if the type of the complex arguments match what's expected by the motive, and diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index b357c6e39f..901e78dd22 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/src/Lean/Elab/Tactic/Try.lean @@ -25,7 +25,7 @@ namespace Try /-! `evalSuggest` is a `evalTactic` variant that returns suggestions after executing a tactic built using -combinatiors such as `first`, `attempt_all`, `<;>`, `;`, and `try`. +combinators such as `first`, `attempt_all`, `<;>`, `;`, and `try`. -/ /-- Returns `true` if `fvarId` has an accessible name. -/ diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index efd52d0e12..d77fdafce4 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -2404,7 +2404,7 @@ Evaluates the given declaration under the given environment to a value of the gi This function is only safe to use if the type matches the declaration's type in the environment and if `enableInitializersExecution` has been used before importing any modules. -If `checkMeta` is true (the default), the function checks that all referenced imported contants are +If `checkMeta` is true (the default), the function checks that all referenced imported constants are marked or imported as `meta` or otherwise fails with an error. It should only be set to `false` in cases where it is acceptable for code to work only in the language server, where more IR is loaded, such as in `#eval`. diff --git a/src/Lean/ErrorExplanations/InvalidField.lean b/src/Lean/ErrorExplanations/InvalidField.lean index 89ea078d9e..1942d10daa 100644 --- a/src/Lean/ErrorExplanations/InvalidField.lean +++ b/src/Lean/ErrorExplanations/InvalidField.lean @@ -15,7 +15,7 @@ and that it wasn't possible to understand the identifier as a field. Lean's field notation is very powerful, but this can also make it confusing: the expression `color.value` can either be a single [identifier](lean-manual://section/identifiers-and-resolution), -it can be a reference to the [field of a structure](lean-manual://section/structure-fiels), and it +it can be a reference to the [field of a structure](lean-manual://section/structure-fields), and it and be a calling a function on the value `color` with [generalized field notation](lean-manual://section/generalized-field-notation). diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 325424fd7b..f2cddd270a 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1867,7 +1867,7 @@ def withLetDecl (name : Name) (type : Expr) (val : Expr) (k : Expr → n α) (no /-- Runs `k x` with the local declaration ` : := ` added to the local context, where `x` is the new free variable. Afterwards, the result is wrapped in the given `let`/`have` expression (according to the value of `nondep`). -- If `usedLetOnly := true` (the default) then the the `let`/`have` is not created if the variable is unused. +- If `usedLetOnly := true` (the default) then the `let`/`have` is not created if the variable is unused. -/ def mapLetDecl [MonadLiftT MetaM n] (name : Name) (type : Expr) (val : Expr) (k : Expr → n Expr) (nondep : Bool := false) (kind : LocalDeclKind := .default) (usedLetOnly : Bool := true) : n Expr := withLetDecl name type val (nondep := nondep) (kind := kind) fun x => do diff --git a/src/Lean/Meta/CasesInfo.lean b/src/Lean/Meta/CasesInfo.lean index 9913b52672..98bb9d8c49 100644 --- a/src/Lean/Meta/CasesInfo.lean +++ b/src/Lean/Meta/CasesInfo.lean @@ -16,7 +16,7 @@ This modules defines the `CasesInfo` data structure and functions to obtain it. It contains information about the structure of casesOn-like functions, namely of * Plain `.casesOn` (one alternative per constructor) -* Per-constructor eliminiations (with side condition, one alternative only) +* Per-constructor eliminations (with side condition, one alternative only) * Sparse cases-on (only some constructors, with a catch-all) It recognizes `.casesOn` by using `isCasesOnRecursor` (name + `isAuxDecl` env ext), and the others diff --git a/src/Lean/Meta/Constructions/CasesOnSameCtor.lean b/src/Lean/Meta/Constructions/CasesOnSameCtor.lean index 8e0d41e322..cc01a344a3 100644 --- a/src/Lean/Meta/Constructions/CasesOnSameCtor.lean +++ b/src/Lean/Meta/Constructions/CasesOnSameCtor.lean @@ -23,7 +23,7 @@ namespace Lean open Meta /-- -Helper for `mkCasesOnSameCtor` that constructs a heterogenous matcher (indices may differ) +Helper for `mkCasesOnSameCtor` that constructs a heterogeneous matcher (indices may differ) and does not include the equality proof in the motive (so it's not a the shape of a matcher) yet. -/ public def mkCasesOnSameCtorHet (declName : Name) (indName : Name) : MetaM Unit := do @@ -128,7 +128,7 @@ this module can be dropped. Note that for some data types where the indices determine the constructor (e.g. `Vec`), this leads to less efficient code than the normal matcher, as this needs to read the constructor tag on both -arguments, wheras the normal matcher produces code that reads just the first argument’s tag, and +arguments, whereas the normal matcher produces code that reads just the first argument’s tag, and then boldly reads the second argument’s fields. -/ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit := do diff --git a/src/Lean/Meta/Constructions/CtorElim.lean b/src/Lean/Meta/Constructions/CtorElim.lean index db1cecb759..bac22d2c64 100644 --- a/src/Lean/Meta/Constructions/CtorElim.lean +++ b/src/Lean/Meta/Constructions/CtorElim.lean @@ -232,7 +232,7 @@ public def mkCtorElim (indName : Name) : MetaM Unit := do Generate the `.toCtorIdx` and `.ctor.elim` definitions for the given inductive. This attribute is only meant to be used in `Init.Prelude` to build these constructions for -types where we did not generate them imediatelly (due to `set_option genCtorIdx false`). +types where we did not generate them immediately (due to `set_option genCtorIdx false`). -/ @[builtin_doc] builtin_initialize registerBuiltinAttribute { diff --git a/src/Lean/Meta/Constructions/SparseCasesOn.lean b/src/Lean/Meta/Constructions/SparseCasesOn.lean index f0aa041e56..b5de031490 100644 --- a/src/Lean/Meta/Constructions/SparseCasesOn.lean +++ b/src/Lean/Meta/Constructions/SparseCasesOn.lean @@ -41,7 +41,7 @@ were not matched. Using a single hypothesis like this, rather than many hypothes This function is implemented with a simple call to `.rec`, i.e. no clever branching on the constructor index. The compiler has native support for these sparse matches anyways, and kernel reduction would -not benefit from from a more sophisticated implementan unless it has itself native support for +not benefit from a more sophisticated implementation unless it has itself native support for `.ctorIdx` and constructor elimination functions. -/ public def mkSparseCasesOn (indName : Name) (ctors : Array Name) : MetaM Name := do diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index 0f0aac19d2..4e89ec017d 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean @@ -111,7 +111,7 @@ builtin_initialize registerReservedNamePredicate fun env n => Id.run do if let some (declName, suffix) := declFromEqLikeName env n then -- The reserved name predicate has to be precise, as `resolveExact` -- will believe it. So make sure that `n` is exactly the name we expect, - -- including the privat prefix. + -- including the private prefix. n == mkEqLikeNameFor env declName suffix else false diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 378de18b4f..bf24181dab 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -1753,7 +1753,7 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do Without the proof irrelevance check, this example timeouts. Recall that: 1- The elaborator has a pending list of things to do: Tactics, TC, etc. - 2- The elaborator only tries tactics after it tried to solve pending TC problems, delayed elaboratio, etc. + 2- The elaborator only tries tactics after it tried to solve pending TC problems, delayed elaboration, etc. The motivation: avoid unassigned metavariables in goals. 3- Each pending tactic goal is represented as a metavariable. It is marked as `syntheticOpaque` to make it clear that it should not be assigned by unification. diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index 30a9f9794d..dfa444e78e 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -15,7 +15,7 @@ import Lean.Meta.Tactic.SolveByElim # The `below` and `brecOn` constructions for inductive predicates This module defines the `below` and `brecOn` constructions for inductive predicates. -While the `brecOn` construction for inductive predicates is structurally indentical to the one for +While the `brecOn` construction for inductive predicates is structurally identical to the one for regular types apart from only eliminating to propositions, the `below` construction is changed since it is unlike for types not possible to eliminate proofs of inductive predicates to `Prop`s containing nested proofs. Instead, each `below` declaration is defined as an inductive type with one diff --git a/src/Lean/Meta/Match/AltTelescopes.lean b/src/Lean/Meta/Match/AltTelescopes.lean index 4d9511103d..1cca69300e 100644 --- a/src/Lean/Meta/Match/AltTelescopes.lean +++ b/src/Lean/Meta/Match/AltTelescopes.lean @@ -15,8 +15,8 @@ import Lean.Meta.AppBuilder public section /-! -This module has telescope functions for macher alts. They are primariliy used -in `Match.MatchEqs`, but also in `MatcherApp.Transform`, hence the sparate module. +This module has telescope functions for matcher alts. They are primarily used +in `Match.MatchEqs`, but also in `MatcherApp.Transform`, hence the separate module. -/ namespace Lean.Meta.Match diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index 5ae8b9026e..d977f031c8 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -35,14 +35,14 @@ def Overlaps.overlapping (o : Overlaps) (overlapped : Nat) : Array Nat := | none => #[] /-- -Informatino about the parameter structure for the alternative of a matcher or splitter. +Information about the parameter structure for the alternative of a matcher or splitter. -/ structure AltParamInfo where - /-- Actual fields (not incuding discr eqns) -/ + /-- Actual fields (not including discr eqns) -/ numFields : Nat /-- Overlap assumption (for splitters only) -/ numOverlaps : Nat - /-- Whether this alternatie has an artifcial `Unit` parameter -/ + /-- Whether this alternative has an artificial `Unit` parameter -/ hasUnitThunk : Bool deriving Inhabited, Repr, BEq diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index eb6a36cd29..62a25576e7 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -516,7 +516,7 @@ def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) Like `mkLambdaFVars (usedOnly := true)`, but * silently skips expression in `xs` that are not `.isFVar` - * also skips let-bound variabls + * also skips let-bound variables * returns a mask (same size as `xs`) indicating which variables have been abstracted (`true` means was abstracted). diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index e1036b821e..6b0c3dc9bf 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -61,7 +61,7 @@ def addCongrTable (e : Expr) : GoalM Unit := do pushEqHEq e e' congrPlaceholderProof if (← swapCgrRepr e e') then /- - Recall that `isDiseq` and `mkDiseqProof?` are implemented using the the congruence table. + Recall that `isDiseq` and `mkDiseqProof?` are implemented using the congruence table. So, if `e` is an equality `a = b`, and is the equivalence class of `False`, but `e'` is not, we **must** make `e` the representative of the congruence class. The equivalence classes of `e` and `e'` will be merged eventually since we used `pushEqHEq` above, diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 6946b9a050..67215c5976 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -351,7 +351,7 @@ def simpForall (e : Expr) : SimpM Result := withParent e do : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) ``` Remark: we should consider whether we want to add congruence lemma support for arbitrary `forall`-expressions. - Then, the theroem above can be marked as `@[congr]` and the following code deleted. + Then, the theorem above can be marked as `@[congr]` and the following code deleted. -/ let p₁ := domain let p₂ := rd.expr diff --git a/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean index a136672ad3..3b4569c3c6 100644 --- a/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean +++ b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean @@ -22,7 +22,7 @@ macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)? let procStr := procId.getId.toString let procIdParser := mkIdentFrom procId (`Parser.Attr ++ procId.getId) let procDescr := quote s!"simproc set for {procId.getId.toString}" - -- TODO: better docDomment for simprocs + -- TODO: better docComment for simprocs `($[$doc:docComment]? initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr $(quote id.getId) $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (prio)? : attr /-- Simplification procedure -/ diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index 76b29b3210..da5ab0da54 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -16,7 +16,7 @@ import Lean.ExtraModUses public section /-! -This module contains types to manages simp theorems and sets theirof. +This module contains types to manages simp theorems and sets thereof. Overview of types in this module: @@ -39,7 +39,7 @@ namespace Lean.Meta register_builtin_option backward.dsimp.useDefEqAttr : Bool := { defValue := true - descr := "Use `defeq` attribute rather than checking theorem body to decide whether a theroem \ + descr := "Use `defeq` attribute rather than checking theorem body to decide whether a theorem \ can be used in `dsimp` or with `implicitDefEqProofs`." } diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 3ad4c04592..336e2676db 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -101,7 +101,7 @@ private def throwInternalMisuseError [Monad m] [MonadError m] (msg : MessageData /-- Split works best if all discriminants are already free variables. If they are not, it will generalize them, but that may fail if the motive is dependent. So to avoid that, we first generalize all -non-FVar discriminants that are propositions; because of proof irrelvance, that's much simpler. +non-FVar discriminants that are propositions; because of proof irrelevance, that's much simpler. -/ private partial def generalizeMatchPropDiscrs (mvarId : MVarId) (discrs : Array Expr) : MetaM (Array Expr × MVarId) := mvarId.withContext do let mut mvarId := mvarId diff --git a/src/Lean/Meta/Tactic/UnifyEq.lean b/src/Lean/Meta/Tactic/UnifyEq.lean index 7d51637ae7..e830132513 100644 --- a/src/Lean/Meta/Tactic/UnifyEq.lean +++ b/src/Lean/Meta/Tactic/UnifyEq.lean @@ -58,7 +58,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {}) | some (_, a, b) => /- Remark: we do not check `isDefeq` here because we would fail to substitute equalities - such as `x = t` and `t = x` when `x` and `t` are proofs (proof irrelanvance). + such as `x = t` and `t = x` when `x` and `t` are proofs (proof irrelevance). -/ /- Remark: we use `let rec` here because otherwise the compiler would generate an insane amount of code. We can remove the `rec` after we fix the eagerly inlining issue in the compiler. -/ diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index 3c9d0d68be..34488a57b3 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -191,7 +191,7 @@ def zetaDeltaFVars (e : Expr) (fvars : Array FVarId) : MetaM Expr := def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do withoutModifyingEnv do let env ← getEnv - -- There might have been nested proof abstractions, which yield private helper theoresms, so + -- There might have been nested proof abstractions, which yield private helper theorems, so -- make sure we can find them. They will later be re-abstracted again. let biggerEnv := biggerEnv.setExporting false setEnv biggerEnv -- `e` has declarations from `biggerEnv` that are not in `env` diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 8f07060e83..6ef51f8174 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -259,7 +259,7 @@ withTraceNode `isPosTrace (msg := (return m!"{ExceptToEmoji.toEmoji ·} checking return 0 < x ``` -The `cls`, `collapsed`, and `tag` arguments are fowarded to the constructor of `TraceData`. +The `cls`, `collapsed`, and `tag` arguments are forwarded to the constructor of `TraceData`. -/ def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : Name) (msg : Except ε α → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do diff --git a/src/Std/Data/DTreeMap/Raw/Basic.lean b/src/Std/Data/DTreeMap/Raw/Basic.lean index e5c7e15121..8d412a603d 100644 --- a/src/Std/Data/DTreeMap/Raw/Basic.lean +++ b/src/Std/Data/DTreeMap/Raw/Basic.lean @@ -733,8 +733,8 @@ def inter (t₁ t₂ : Raw α β cmp) : Raw α β cmp := instance : Inter (Raw α β cmp) := ⟨inter⟩ /-- -Computes the diffrence of the given tree maps. -This function always iteraters through the smaller map. +Computes the difference of the given tree maps. +This function always iterates through the smaller map. -/ def diff (t₁ t₂ : Raw α β cmp) : Raw α β cmp := letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.diff! t₂.inner⟩ diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean index 87e967d072..1a55e06802 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean @@ -13,7 +13,7 @@ public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred /-! This module contains the logic to turn a `BVLogicalExpr` into an `AIG` with maximum subterm sharing, through the use of a cache that re-uses sub-circuits if possible. Additionally a term level cache -is used to prevent rerunning bitblasting on commong bitvector subexpressions. +is used to prevent rerunning bitblasting on common bitvector subexpressions. -/ namespace Std.Tactic.BVDecide diff --git a/src/lake/Lake/Build/Context.lean b/src/lake/Lake/Build/Context.lean index c2838fe85a..1ceb762562 100644 --- a/src/lake/Lake/Build/Context.lean +++ b/src/lake/Lake/Build/Context.lean @@ -24,7 +24,7 @@ public structure BuildConfig extends LogConfig where verbosity : Verbosity := .normal /-- Whether to print a message when the build finishes successfully (if not quiet). -/ showSuccess : Bool := false - /-- File to save input-to-output mappings from the build of the worksoace's root -/ + /-- File to save input-to-output mappings from the build of the workspace's root -/ outputsFile? : Option FilePath := none /-- diff --git a/src/lake/Lake/Build/Target/Fetch.lean b/src/lake/Lake/Build/Target/Fetch.lean index 2c10db43db..65b2000d14 100644 --- a/src/lake/Lake/Build/Target/Fetch.lean +++ b/src/lake/Lake/Build/Target/Fetch.lean @@ -83,7 +83,7 @@ where /-- Fetches the target specified by this key, resolving gaps as needed. -* A missing package (i.e., `Name.anoanmoyus`) is filled in with `defaultPkg`. +* A missing package (i.e., `Name.anonymous`) is filled in with `defaultPkg`. * Facets are qualified by the their input target's kind, and missing facets are replaced by their kind's `default`. * Package targets ending in `moduleTargetIndicator` are converted to module package targets. diff --git a/src/lake/Lake/Config/ConfigDecl.lean b/src/lake/Lake/Config/ConfigDecl.lean index 7335c66f1a..fef72d6f15 100644 --- a/src/lake/Lake/Config/ConfigDecl.lean +++ b/src/lake/Lake/Config/ConfigDecl.lean @@ -138,10 +138,10 @@ public abbrev ExternLibDecl := KConfigDecl ExternLib.configKind (self : NConfigDecl p n) : Option (OpaqueTargetConfig p n) := cast (by rw [self.name_eq]) self.toPConfigDecl.opaqueTargetConfig? -/-- A input file declaration from a configuration written in Lean. -/ +/-- An input file declaration from a configuration written in Lean. -/ public abbrev InputFileDecl := KConfigDecl InputFile.configKind -/-- A inpurt directory declaration from a configuration written in Lean. -/ +/-- An input directory declaration from a configuration written in Lean. -/ public abbrev InputDirDecl := KConfigDecl InputDir.configKind public instance : TypeName LeanLibDecl := unsafe (.mk _ ``LeanLibDecl) diff --git a/src/lake/Lake/Config/InputFileConfig.lean b/src/lake/Lake/Config/InputFileConfig.lean index ea621a7f18..f883135651 100644 --- a/src/lake/Lake/Config/InputFileConfig.lean +++ b/src/lake/Lake/Config/InputFileConfig.lean @@ -50,7 +50,7 @@ public configuration InputDirConfig (name : Name) where text : Bool := false /- Includes only the files from the directory - whose paths statisify the pattern. + whose paths satisfy the pattern. Defaults to including every file. -/ diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index c3886fb64e..c221b5c116 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/src/lake/Lake/Config/Workspace.lean @@ -249,7 +249,7 @@ public def augmentedLeanSrcPath (self : Workspace) : SearchPath := The detected `sharedLibPathEnv` value of the environment augmented with the workspace's `libPath` and Lean installation's shared library directories. -The order is Lean's, the workspace's, and then the enviroment's. +The order is Lean's, the workspace's, and then the environment's. Lean's comes first because Lean needs to load its own shared libraries from this path. Giving the workspace greater precedence can break this (e.g., when bootstrapping), -/ diff --git a/tests/lean/grind/experiments/bitvec.lean b/tests/lean/grind/experiments/bitvec.lean index 0c36441602..e0ca1c801c 100644 --- a/tests/lean/grind/experiments/bitvec.lean +++ b/tests/lean/grind/experiments/bitvec.lean @@ -5190,7 +5190,7 @@ theorem msb_eq_toNat {x : BitVec w}: simp only [msb_eq_decide, ge_iff_le] /-- Negating a bitvector created from a natural number equals -creating a bitvector from the the negative of that number. +creating a bitvector from the negative of that number. -/ theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} : - BitVec.ofNat w x = BitVec.ofInt w (- x) := by diff --git a/tests/lean/run/grind_bitvec2.lean b/tests/lean/run/grind_bitvec2.lean index c1bccd0c62..b96d0121f0 100644 --- a/tests/lean/run/grind_bitvec2.lean +++ b/tests/lean/run/grind_bitvec2.lean @@ -4319,7 +4319,7 @@ theorem msb_eq_toNat {x : BitVec w}: simp only [msb_eq_decide, ge_iff_le] /-- Negating a bitvector created from a natural number equals -creating a bitvector from the the negative of that number. +creating a bitvector from the negative of that number. -/ theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} : - BitVec.ofNat w x = BitVec.ofInt w (- x) := by diff --git a/tests/lean/run/grind_qsort.lean b/tests/lean/run/grind_qsort.lean index 1fdc9efe6f..a4ef413bb8 100644 --- a/tests/lean/run/grind_qsort.lean +++ b/tests/lean/run/grind_qsort.lean @@ -51,14 +51,14 @@ grind_pattern List.Perm.trans => l₁ ~ l₂, l₁ ~ l₃ grind_pattern Array.Perm.trans => xs ~ ys, xs ~ zs grind_pattern Vector.Perm.trans => xs ~ ys, xs ~ zs -/-- Variant of `List.Perm.take` specifying the the permutation is constant after `i` elementwise. -/ +/-- Variant of `List.Perm.take` specifying the permutation is constant after `i` elementwise. -/ theorem _root_.List.Perm.take_of_getElem {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, i ≤ j → (_ : j < l₁.length) → l₁[j] = l₂[j]'(by have := h.length_eq; omega)) : l₁.take i ~ l₂.take i := by apply h.take_of_getElem? sorry -/-- Variant of `List.Perm.drop` specifying the the permutation is constant before `i` elementwise. -/ +/-- Variant of `List.Perm.drop` specifying the permutation is constant before `i` elementwise. -/ theorem _root_.List.Perm.drop_of_getElem {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, j < i → (_ : j < l₁.length) → l₁[j] = l₂[j]'(by have := h.length_eq; omega)) : l₁.drop i ~ l₂.drop i := by diff --git a/tests/lean/run/issue8939wf.lean b/tests/lean/run/issue8939wf.lean index 8e3ba7f69d..a2ba230aac 100644 --- a/tests/lean/run/issue8939wf.lean +++ b/tests/lean/run/issue8939wf.lean @@ -2,7 +2,7 @@ module /-! variant of issue8939 with well-founded recursion -(Or is this just 8938 showing up with 8939 fixed? anwways, more tests don't hurt) +(Or is this just 8938 showing up with 8939 fixed? anyways, more tests don't hurt) -/ public axiom g : Nat → Nat → Nat diff --git a/tests/lean/run/timeParse.lean b/tests/lean/run/timeParse.lean index b7d630ad24..09de21d9bd 100644 --- a/tests/lean/run/timeParse.lean +++ b/tests/lean/run/timeParse.lean @@ -134,7 +134,7 @@ info: "2024-08-16T01:28:12.000000000+09:00" /-- TM: 1723730627 GMT: Thursday, 15 August 2024 14:03:47 -Your time zone: 15 Aguust 2024 11:03:47 GMT-03:00 +Your time zone: 15 August 2024 11:03:47 GMT-03:00 -/ def localTm : Second.Offset := 1723730627