From 858a9f2d9a6aa0709b062a28bf6b31062232255a Mon Sep 17 00:00:00 2001 From: euprunin Date: Mon, 23 Sep 2024 23:35:33 +0200 Subject: [PATCH] chore: fix spelling mistakes in src/Lean/Elab/ --- src/Lean/Elab/AuxDef.lean | 2 +- src/Lean/Elab/Binders.lean | 2 +- src/Lean/Elab/BuiltinCommand.lean | 2 +- src/Lean/Elab/DeclModifiers.lean | 2 +- src/Lean/Elab/Extra.lean | 6 +++--- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/PreDefinition/Main.lean | 2 +- src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean | 4 ++-- src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean | 2 +- src/Lean/Elab/PreDefinition/Structural/Preprocess.lean | 2 +- src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean | 4 ++-- src/Lean/Elab/PreDefinition/TerminationArgument.lean | 2 +- src/Lean/Elab/PreDefinition/TerminationHint.lean | 2 +- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 2 +- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 8 ++++---- src/Lean/Elab/PreDefinition/WF/Preprocess.lean | 2 +- src/Lean/Elab/RecAppSyntax.lean | 2 +- src/Lean/Elab/SyntheticMVars.lean | 6 +++--- src/Lean/Elab/Tactic/BVDecide.lean | 2 +- src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean | 2 +- src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean | 2 +- src/Lean/Elab/Tactic/Conv/Congr.lean | 2 +- src/Lean/Elab/Tactic/Omega.lean | 2 +- src/Lean/Elab/Tactic/Omega/Core.lean | 2 +- src/Lean/Elab/Tactic/Omega/Frontend.lean | 2 +- src/Lean/Elab/Term.lean | 2 +- 26 files changed, 35 insertions(+), 35 deletions(-) diff --git a/src/Lean/Elab/AuxDef.lean b/src/Lean/Elab/AuxDef.lean index 3dd12700964e..a1f693d2886e 100644 --- a/src/Lean/Elab/AuxDef.lean +++ b/src/Lean/Elab/AuxDef.lean @@ -24,7 +24,7 @@ def elabAuxDef : CommandElab let id := `_aux ++ (← getMainModule) ++ `_ ++ id let id := String.intercalate "_" <| id.components.map (·.toString (escape := false)) let ns ← getCurrNamespace - -- make sure we only add a single component so that scoped workes + -- make sure we only add a single component so that scoped works let id ← mkAuxName (ns.mkStr id) 1 let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id elabCommand <| diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 123c9bf02b0a..ba46e151c1e5 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -650,7 +650,7 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va /- We use `withSynthesize` to ensure that any postponed elaboration problem and nested tactics in `type` are resolved before elaborating `val`. - Resolved: we want to avoid synthethic opaque metavariables in `type`. + Resolved: we want to avoid synthetic opaque metavariables in `type`. Recall that this kind of metavariable is non-assignable, and `isDefEq` may waste a lot of time unfolding declarations before failing. See issue #4051 for an example. diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index f732c7c0608a..e9923af7697d 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -381,7 +381,7 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax): CommandElabM Uni -- Evaluate using term using `MetaEval` class. let elabMetaEval : CommandElabM Unit := do -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure - -- we don't polute the environment with auxliary declarations. + -- we don't pollute the environment with auxliary declarations. -- We have special support for `CommandElabM` to ensure `#eval` can be used to execute commands -- that modify `CommandElabM` state not just the `Environment`. let act : Sum (CommandElabM Unit) (Environment → Options → IO (String × Except IO.Error Environment)) ← diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index c83a015a08d6..ff4612058798 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -120,7 +120,7 @@ section Methods variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] -/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `proctected`, `unsafe`, `noncomputable`, doc string)-/ +/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/ def elabModifiers (stx : Syntax) : m Modifiers := do let docCommentStx := stx[0] let attrsStx := stx[1] diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index 7420dd85dcc4..7e2ae65993d7 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -375,7 +375,7 @@ private def hasHeterogeneousDefaultInstances (f : Expr) (maxType : Expr) (lhs : return false /-- - Return `true` if polymorphic function `f` has a homogenous instance of `maxType`. + Return `true` if polymorphic function `f` has a homogeneous instance of `maxType`. The coercions to `maxType` only makes sense if such instance exists. For example, suppose `maxType` is `Int`, and `f` is `HPow.hPow`. Then, @@ -421,9 +421,9 @@ mutual | .binop ref kind f lhs rhs => /- We only keep applying coercions to `maxType` if `f` is predicate or - `f` has a homogenous instance with `maxType`. See `hasHomogeneousInstance` for additional details. + `f` has a homogeneous instance with `maxType`. See `hasHomogeneousInstance` for additional details. - Remark: We assume `binrel%` elaborator is only used with homogenous predicates. + Remark: We assume `binrel%` elaborator is only used with homogeneous predicates. -/ if (← pure isPred <||> hasHomogeneousInstance f maxType) then return .binop ref kind f (← go lhs f true false) (← go rhs f false false) diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 0c9e261ebe01..4b69e66d9126 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -30,7 +30,7 @@ private def mkUserNameFor (e : Expr) : TermElabM Name := do /-- - Remark: if the discriminat is `Systax.missing`, we abort the elaboration of the `match`-expression. + Remark: if the discriminat is `Syntax.missing`, we abort the elaboration of the `match`-expression. This can happen due to error recovery. Example ``` example : (p ∨ p) → p := fun h => match diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 9bd945c1fe95..137e8c05c8f6 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -104,7 +104,7 @@ Checks consistency of a clique of TerminationHints: * If not all have a hint, the hints are ignored (log error) * If one has `structural`, check that all have it, (else throw error) -* A `structural` shold not have a `decreasing_by` (else log error) +* A `structural` should not have a `decreasing_by` (else log error) -/ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean index c7fa508a9daf..affefd8a90f9 100644 --- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean @@ -119,7 +119,7 @@ def getRecArgInfos (fnName : Name) (xs : Array Expr) (value : Expr) (termArg? : Option TerminationArgument) : MetaM (Array RecArgInfo × MessageData) := do lambdaTelescope value fun ys _ => do if let .some termArg := termArg? then - -- User explictly asked to use a certain argument, so throw errors eagerly + -- User explicitly asked to use a certain argument, so throw errors eagerly let recArgInfo ← withRef termArg.ref do mapError (f := (m!"cannot use specified parameter for structural recursion:{indentD ·}")) do getRecArgInfo fnName xs.size (xs ++ ys) (← termArg.structuralArg) @@ -189,7 +189,7 @@ def argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr) if (← group.isDefEq recArgInfo.indGroupInst) then return (.some recArgInfo) - -- Can this argument be understood as the auxillary type former of a nested inductive? + -- Can this argument be understood as the auxiliary type former of a nested inductive? if nestedTypeFormers.isEmpty then return .none lambdaTelescope value fun ys _ => do let x := (xs++ys)[recArgInfo.recArgPos]! diff --git a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean index 78354fa8170b..457a406589d4 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean @@ -13,7 +13,7 @@ This module contains the types * `IndGroupInst` which extends `IndGroupInfo` with levels and parameters to indicate a instantiation of the group. -One purpose of this abstraction is to make it clear when a fuction operates on a group as +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. -/ diff --git a/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean b/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean index 4107944870b3..dc3d1ddb3197 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean @@ -17,7 +17,7 @@ private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool := false /-- -Preprocesses the expessions to improve the effectiveness of `elimRecursion`. +Preprocesses the expressions to improve the effectiveness of `elimRecursion`. * Beta reduce terms where the recursive function occurs in the lambda term. Example: diff --git a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean index 2d5329324c21..0453fa98592e 100644 --- a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean @@ -31,7 +31,7 @@ structure RecArgInfo where indGroupInst : IndGroupInst /-- index of the inductive datatype of the argument we are recursing on. - If `< indAll.all`, a normal data type, else an auxillary data type due to nested recursion + If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion -/ indIdx : Nat deriving Inhabited @@ -52,7 +52,7 @@ def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array E return (indexMajorArgs, otherArgs) /-- -Name of the recursive data type. Assumes that it is not one of the auxillary ones. +Name of the recursive data type. Assumes that it is not one of the auxiliary ones. -/ def RecArgInfo.indName! (info : RecArgInfo) : Name := info.indGroupInst.all[info.indIdx]! diff --git a/src/Lean/Elab/PreDefinition/TerminationArgument.lean b/src/Lean/Elab/PreDefinition/TerminationArgument.lean index c83e47ffbedb..02279088410c 100644 --- a/src/Lean/Elab/PreDefinition/TerminationArgument.lean +++ b/src/Lean/Elab/PreDefinition/TerminationArgument.lean @@ -112,7 +112,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi let stxBody ← Delaborator.delab let hole : TSyntax `Lean.Parser.Term.hole ← `(hole|_) - -- any variable not mentioned syntatically (it may appear in the `Expr`, so do not just use + -- any variable not mentioned syntactically (it may appear in the `Expr`, so do not just use -- `e.bindingBody!.hasLooseBVar`) should be delaborated as a hole. let vars : TSyntaxArray [`ident, `Lean.Parser.Term.hole] := Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars diff --git a/src/Lean/Elab/PreDefinition/TerminationHint.lean b/src/Lean/Elab/PreDefinition/TerminationHint.lean index 757d388d55a0..29ce520555d3 100644 --- a/src/Lean/Elab/PreDefinition/TerminationHint.lean +++ b/src/Lean/Elab/PreDefinition/TerminationHint.lean @@ -45,7 +45,7 @@ structure TerminationHints where decreasingBy? : Option DecreasingBy /-- Here we record the number of parameters past the `:`. It is set by - `TerminationHints.rememberExtraParams` and used as folows: + `TerminationHints.rememberExtraParams` and used as follows: * When we guess the termination argument in `GuessLex` and want to print it in surface-syntax compatible form. diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 41ad8bda2059..a8bea93c8b34 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -66,7 +66,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do else if let some mvarIds ← splitTarget? mvarId then mvarIds.forM go else - -- At some point in the past, we looked for occurences of Wf.fix to fold on the + -- At some point in the past, we looked for occurrences of Wf.fix to fold on the -- LHS (introduced in 096e4eb), but it seems that code path was never used, -- so #3133 removed it again (and can be recovered from there if this was premature). throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}" diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 2442b9a164fa..bfe4d2d04254 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -29,7 +29,7 @@ if given, or the default `decreasing_tactic`. For mutual recursion, a single measure is not just one parameter, but one from each recursive function. Enumerating these can lead to a combinatoric explosion, so we bound -the nubmer of measures tried. +the number of measures tried. In addition to measures derived from `sizeOf xᵢ`, it also considers measures that assign an order to the functions themselves. This way we can support mutual @@ -42,7 +42,7 @@ guessed lexicographic order. The following optimizations are applied to make this feasible: -1. The crucial optimiziation is to look at each argument of each recursive call +1. The crucial optimization is to look at each argument of each recursive call _once_, try to prove `<` and (if that fails `≤`), and then look at that table to pick a suitable measure. @@ -80,7 +80,7 @@ register_builtin_option showInferredTerminationBy : Bool := { /-- -Given a predefinition, return the variabe names in the outermost lambdas. +Given a predefinition, return the variable names in the outermost lambdas. Includes the “fixed prefix”. The length of the returned array is also used to determine the arity @@ -550,7 +550,7 @@ where failure /-- -Enumerate all meausures we want to try. +Enumerate all measures we want to try. All arguments (resp. combinations thereof) and possible orderings of functions (if more than one) diff --git a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean index ad856ae13214..27cdd7b93bf7 100644 --- a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean +++ b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean @@ -17,7 +17,7 @@ private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool := false /-- -Preprocesses the expessions to improve the effectiveness of `wfRecursion`. +Preprocesses the expressions to improve the effectiveness of `wfRecursion`. * Floats out the RecApp markers. Example: diff --git a/src/Lean/Elab/RecAppSyntax.lean b/src/Lean/Elab/RecAppSyntax.lean index f537b1d85b2f..8a638f02b7cc 100644 --- a/src/Lean/Elab/RecAppSyntax.lean +++ b/src/Lean/Elab/RecAppSyntax.lean @@ -29,7 +29,7 @@ def getRecAppSyntax? (e : Expr) : Option Syntax := | _ => none /-- -Checks if the `MData` is for a recursive applciation. +Checks if the `MData` is for a recursive application. -/ def MData.isRecApp (d : MData) : Bool := d.contains recAppKey diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 2f35b25dcc00..1eb11524483c 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -21,7 +21,7 @@ private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSo elabTerm stx expectedType? false /-- - Try to elaborate `stx` that was postponed by an elaboration method using `Expection.postpone`. + Try to elaborate `stx` that was postponed by an elaboration method using `Exception.postpone`. It returns `true` if it succeeded, and `false` otherwise. It is used to implement `synthesizeSyntheticMVars`. -/ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool := @@ -86,7 +86,7 @@ private def synthesizePendingInstMVar (instMVar : MVarId) (extraErrorMsg? : Opti example (a : Int) (b c : Nat) : a = ↑b - ↑c := sorry ``` We have two pending coercions for the `↑` and `HSub ?m.220 ?m.221 ?m.222`. - When we did not use a backtracking search here, then the homogenous default instance for `HSub`. + When we did not use a backtracking search here, then the homogeneous default instance for `HSub`. ``` instance [Sub α] : HSub α α α where ``` @@ -306,7 +306,7 @@ inductive PostponeBehavior where | no /-- Synthectic metavariables associated with type class resolution can be postponed. - Motivation: this kind of metavariable are not synthethic opaque, and can be assigned by `isDefEq`. + Motivation: this kind of metavariable are not synthetic opaque, and can be assigned by `isDefEq`. Unviverse constraints can also be postponed. -/ | «partial» diff --git a/src/Lean/Elab/Tactic/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide.lean index 9f8c517b0555..eeee215474a6 100644 --- a/src/Lean/Elab/Tactic/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide.lean @@ -71,7 +71,7 @@ For the second kind more steps are involved: 3. Verify that algorithm in `Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas`. 4. Integrate it with either the expression or predicate bitblaster and use the proof above to verify it. 5. Add simplification lemmas for the primitive to `bv_normalize` in `Std.Tactic.BVDecide.Normalize`. - If there are mutliple ways to write the primitive (e.g. with TC based notation and without) you + If there are multiple ways to write the primitive (e.g. with TC based notation and without) you should normalize for one notation here. 6. Add the reflection code to `Lean.Elab.Tactic.BVDecide.Frontend.BVDecide` 7. Add a test! diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean index 653fab300b7e..e80ab3b297e0 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean @@ -24,7 +24,7 @@ register_builtin_option sat.solver : String := { defValue := "" descr := "Name of the SAT solver used by Lean.Elab.Tactic.BVDecide tactics.\n - 1. If this is set to something besides the emtpy string they will use that binary.\n + 1. If this is set to something besides the empty string they will use that binary.\n 2. If this is set to the empty string they will check if there is a cadical binary next to the\ executing program. Usually that program is going to be `lean` itself and we do ship a\ `cadical` next to it.\n diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index 048bc15c0680..6d2dae182676 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -270,7 +270,7 @@ structure Result where -/ simpTrace : Simp.Stats /-- - If the normalization step was not enough to solve the goal this contaisn the LRAT proof + If the normalization step was not enough to solve the goal this contains the LRAT proof certificate. -/ lratCert : Option LratCert diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index de4dee1bc55a..167aa349f48b 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -77,7 +77,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) : -- mvarIds is the list of goals produced by congr. We only want to change the one at position `i` -- so this closes all other equality goals with `rfl.`. There are non-equality goals produced --- by `congr` (e.g. dependent instances), thes are kept as goals. +-- by `congr` (e.g. dependent instances), these are kept as goals. private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) : TacticM Unit := do if i >= 0 then diff --git a/src/Lean/Elab/Tactic/Omega.lean b/src/Lean/Elab/Tactic/Omega.lean index f8f6bed5e1dd..13252092bdec 100644 --- a/src/Lean/Elab/Tactic/Omega.lean +++ b/src/Lean/Elab/Tactic/Omega.lean @@ -39,7 +39,7 @@ The `omega` tactic pre-processes the hypotheses in the following ways: * If `x / m` appears, for some `x : Int` and literal `m : Nat`, replace `x / m` with a new variable `α` and add the constraints `0 ≤ - m * α + x ≤ m - 1`. -* If `x % m` appears, similarly, introduce the same new contraints +* If `x % m` appears, similarly, introduce the same new constraints but replace `x % m` with `- m * α + x`. * Split conjunctions, existentials, and subtypes. * Record, for each appearance of `(a - b : Int)` with `a b : Nat`, the disjunction diff --git a/src/Lean/Elab/Tactic/Omega/Core.lean b/src/Lean/Elab/Tactic/Omega/Core.lean index 561f38e1e146..4595a9b772b1 100644 --- a/src/Lean/Elab/Tactic/Omega/Core.lean +++ b/src/Lean/Elab/Tactic/Omega/Core.lean @@ -49,7 +49,7 @@ inductive Justification : Constraint → Coeffs → Type | combo {s t x y} (a : Int) (j : Justification s x) (b : Int) (k : Justification t y) : Justification (Constraint.combo a s b t) (Coeffs.combo a x b y) /-- - The justification for the constraing constructed using "balanced mod" while + The justification for the constraint constructed using "balanced mod" while eliminating an equality. -/ | bmod (m : Nat) (r : Int) (i : Nat) {x} (j : Justification (.exact r) x) : diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 6c5dc7faa93e..ba873bba8e94 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -322,7 +322,7 @@ where end namespace MetaProblem -/-- The trivial `MetaProblem`, with no facts to processs and a trivial `Problem`. -/ +/-- The trivial `MetaProblem`, with no facts to process and a trivial `Problem`. -/ def trivial : MetaProblem where problem := {} diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 60a176fcfc22..714c57a01c13 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1045,7 +1045,7 @@ def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM logException ex pure syntheticSorry -/-- If `mayPostpone == true`, throw `Expection.postpone`. -/ +/-- If `mayPostpone == true`, throw `Exception.postpone`. -/ def tryPostpone : TermElabM Unit := do if (← read).mayPostpone then throwPostpone