diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 70eaf6ef21..9d9169350d 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1261,7 +1261,7 @@ def elabExplicitUnivs (lvls : Array Syntax) : TermElabM (List Level) := do - When we elaborate choice nodes (and overloaded identifiers), we track multiple results using the `observing x` combinator. The `observing x` executes `x` and returns a `TermElabResult`. -`observing `x does not check for synthetic sorry's, just an exception. Thus, it may think `x` worked when it didn't +`observing x` does not check for synthetic sorry's, just an exception. Thus, it may think `x` worked when it didn't if a synthetic sorry was introduced. We decided that checking for synthetic sorrys at `observing` is not a good solution because it would not be clear to decide what the "main" error message for the alternative is. When the result contains a synthetic `sorry`, it is not clear which error message corresponds to the `sorry`. Moreover, while executing `x`, many diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 9ed56cc650..7a6e2e1447 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -231,7 +231,7 @@ private def reportStuckSyntheticMVars (ignoreStuckTC := false) : TermElabM Unit for mvarId in pendingMVars do reportStuckSyntheticMVar mvarId ignoreStuckTC -private def getSomeSynthethicMVarsRef : TermElabM Syntax := do +private def getSomeSyntheticMVarsRef : TermElabM Syntax := do for mvarId in (← get).pendingMVars do if let some decl ← getSyntheticMVarDecl? mvarId then if decl.stx.getPos?.isSome then @@ -395,7 +395,7 @@ mutual -/ partial def synthesizeSyntheticMVars (mayPostpone := true) (ignoreStuckTC := false) : TermElabM Unit := do let rec loop (_ : Unit) : TermElabM Unit := do - withRef (← getSomeSynthethicMVarsRef) <| withIncRecDepth do + withRef (← getSomeSyntheticMVarsRef) <| withIncRecDepth do unless (← get).pendingMVars.isEmpty do if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) then loop () diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 53032df034..6c633f18ec 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -92,7 +92,7 @@ def sortMVarIdsByIndex [MonadMCtx m] [Monad m] (mvarIds : List MVarId) : m (List def withCollectingNewGoalsFrom (k : TacticM Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := /- When `allowNaturalHoles = true`, unassigned holes should become new metavariables, including `_`s. - Thus, we set `holesAsSynthethicOpaque` to true if it is not already set to `true`. + Thus, we set `holesAsSyntheticOpaque` to true if it is not already set to `true`. See issue #1681. We have the tactic ``` `refine' (fun x => _) @@ -246,7 +246,7 @@ def elabTermForApply (stx : Syntax) (mayPostpone := true) : TacticM Expr := do By disabling "error to sorry", we also limit ourselves to at most one error at `t[h']`. - By disabling "error to sorry", we also miss the opportunity to catch mistakes is tactic code such as + By disabling "error to sorry", we also miss the opportunity to catch mistakes in tactic code such as `first | apply nonsensical-term | assumption` This should not be a big problem for the `apply` tactic since we usually provide small terms there. @@ -317,7 +317,7 @@ def evalApplyLikeTactic (tac : MVarId → Expr → MetaM (List MVarId)) (e : Syn withTransparency TransparencyMode.all <| evalTactic stx[1] /-- - Elaborate `stx`. If it a free variable, return it. Otherwise, assert it, and return the free variable. + Elaborate `stx`. If it is a free variable, return it. Otherwise, assert it, and return the free variable. Note that, the main goal is updated when `Meta.assert` is used in the second case. -/ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId := withMainContext do diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index e2d699aa31..0a0e60d54d 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -211,7 +211,7 @@ structure Context where saveRecAppSyntax : Bool := true /-- If `holesAsSyntheticOpaque` is `true`, then we mark metavariables associated - with `_`s as `synthethicOpaque` if they do not occur in patterns. + with `_`s as `syntheticOpaque` if they do not occur in patterns. This option is useful when elaborating terms in tactics such as `refine'` where we want holes there to become new goals. See issue #1681, we have `refine' (fun x => _) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index ad4eb4cc47..2a46eea3fe 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -1538,9 +1538,9 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do However, pattern annotations (`inaccessible?` and `patternWithRef?`) must be consumed. The frontend relies on the fact that is must not be propagated by `isDefEq`. Thus, we consume it here. This is a bit hackish since it is very adhoc. - We might other annotations in the future that we should not preserve. - Perhaps, we should mark the annotation we do want to preserve ones - (e.g., hints for the pretty printer), and consume all other + We might have other annotations in the future that we should not preserve. + Perhaps, we should mark the annotations we do want to preserve + (e.g., hints for the pretty printer), and consume all others. -/ if let some t := patternAnnotation? t then isDefEqQuick t s @@ -1567,7 +1567,7 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do isDefEqQuick t s /- Remark: we do not eagerly synthesize synthetic metavariables when the constraint is not stuck. Reason: we may fail to solve a constraint of the form `?x =?= A` when the synthesized instance - is not definitionally equal to `A`. We left the code here as a remainder of this issue. -/ + is not definitionally equal to `A`. We left the code here as a reminder of this issue. -/ -- else if (← isSynthetic tFn <&&> trySynthPending tFn) then -- let t ← instantiateMVars t -- isDefEqQuick t s @@ -1597,7 +1597,7 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do 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. The motivation: avoid unassigned metavariables in goals. - 3- Each pending tactic goal is represented as a metavariable. It is marked as `synthethicOpaque` to make it clear + 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. 4- When we abstract a term containing metavariables, we often create new metavariables. Example: when abstracting `x` at `f ?m`, we obtain `fun x => f (?m' x)`. If `x` is in the scope of `?m`. @@ -1692,14 +1692,14 @@ where isDefEqSingleton (structName : Name) (s : Expr) (v : Expr) : MetaM Bool := do if isClass (← getEnv) structName then /- - We disable this feature is `structName` is a class. See issue #2011. + We disable this feature if `structName` is a class. See issue #2011. The example at issue #2011, the following weird instance was being generated for `Zero (f x)` ``` (@Zero.mk (f x✝) ((@instZero I (fun i => f i) fun i => inst✝¹ i).1 x✝) ``` where `inst✝¹` is the local instance `[∀ i, Zero (f i)]` - Note that this instance is definitinally equal to the expected nicer + Note that this instance is definitionally equal to the expected nicer instance `inst✝¹ x✝`. However, the nasty instance trigger nasty unification higher order constraints later. @@ -1733,7 +1733,7 @@ private def isDefEqApp (t s : Expr) : MetaM Bool := do let tFn := t.getAppFn let sFn := s.getAppFn if tFn.isConst && sFn.isConst && tFn.constName! == sFn.constName! then - /- See comment at `tryHeuristic` explaining why we processe arguments before universe levels. -/ + /- See comment at `tryHeuristic` explaining why we process arguments before universe levels. -/ if (← checkpointDefEq (isDefEqArgs tFn t.getAppArgs s.getAppArgs <&&> isListLevelDefEqAux tFn.constLevels! sFn.constLevels!)) then return true else @@ -1743,7 +1743,7 @@ private def isDefEqApp (t s : Expr) : MetaM Bool := do else isDefEqOnFailure t s -/-- Return `true` if the types of the given expressions is an inductive datatype with an inductive datatype with a single constructor with no fields. -/ +/-- Return `true` if the type of the given expression is an inductive datatype with a single constructor with no fields. -/ private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do let tType ← whnf (← inferType t) matchConstStruct tType.getAppFn (fun _ => return false) fun _ _ ctorVal => do