max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: correcting typos (#2746)

Browse source
This commit is contained in:
Scott Morrison 2023-10-24 21:55:30 +11:00 • committed by GitHub
parent b00c13a00e
commit d07ec56c33
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
5 changed files with 16 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/App.lean
View file

@ -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

4
src/Lean/Elab/SyntheticMVars.lean
View file

@ -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 ()

6
src/Lean/Elab/Tactic/ElabTerm.lean
View file

@ -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

2
src/Lean/Elab/Term.lean
View file

@ -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 => _)

18
src/Lean/Meta/ExprDefEq.lean
View file

@ -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