From e4ab10dc30a7e819b222814bb331ca938f112cbb Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Mon, 24 Oct 2022 09:29:47 -0400 Subject: [PATCH] doc: fix some typos assinged -> assigned collction -> collection --- src/Lean/Elab/Tactic/Basic.lean | 2 +- src/Lean/Environment.lean | 2 +- src/Lean/Meta/SynthInstance.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index f786d6fc7e..6326e06c85 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -342,7 +342,7 @@ def ensureHasNoMVars (e : Expr) : TacticM Unit := do if e.hasExprMVar then throwError "tactic failed, resulting expression contains metavariables{indentExpr e}" -/-- Close main goal using the given expression. If `checkUnassigned == true`, then `val` must not contain unassinged metavariables. -/ +/-- Close main goal using the given expression. If `checkUnassigned == true`, then `val` must not contain unassigned metavariables. -/ def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do if checkUnassigned then ensureHasNoMVars val diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 201aa3e8ea..f58362b50e 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -101,7 +101,7 @@ the kernel is to type check these declarations and refuse type incorrect ones. T kernel does not allow declarations containing metavariables and/or free variables to be added to an environment. Environments are never destructively updated. -The environment also contains a collction of extensions. For example, the `simp` theorems +The environment also contains a collection of extensions. For example, the `simp` theorems declared by users are stored in an environment extension. Users can declare new extensions using meta-programming. -/ diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 6c914976cd..4111752a18 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -324,7 +324,7 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array def tryResolve (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := do let mvar ← instantiateMVars mvar if !(← hasAssignableMVar mvar) then - /- The metavariable `mvar` may have been assinged when solving typing constraints. + /- The metavariable `mvar` may have been assigned when solving typing constraints. This may happen when a local instance type depends on other local instances. For example, in Mathlib, we have ```