From e84716ba467cf0d631981f057bf1517566cbc643 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Thu, 12 Mar 2026 01:33:49 -0700 Subject: [PATCH 01/13] doc: fix small error in run_meta docstring MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Examples: ```lean4 import Lean open Lean Meta let mvar1 ← mkFreshExprMVar (mkConst `Nat) let e := (mkConst `Nat.succ).app mvar1 -- e is `Nat.succ ?m.773`, `?m.773` is unassigned mvar1.mvarId!.assign (mkNatLit 42) -- e is `Nat.succ ?m.773`, `?m.773` is assigned to `42` let e' ← instantiateMVars e -- e' is `Nat.succ 42`, `?m.773` is assigned to `42` pure 4 def getFinBound (e : Expr) : MetaM (Option Expr) := do let type ← whnf (← inferType e) let_expr Fin bound := type | return none return bound def a : Fin 100 := 42 match ← getFinBound (.const ``a []) with | some limit => IO.println (← ppExpr limit) | none => IO.println "no limit found" ``` --- src/Init/Notation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 86e95cd066d0..ecfe7f13f971 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -722,7 +722,7 @@ syntax (name := runElab) "run_elab " doSeq : command /-- The `run_meta doSeq` command executes code in `MetaM Unit`. -This is the same as `#eval show MetaM Unit from do discard doSeq`. +This is the same as `#eval show MetaM Unit from discard do doSeq`. (This is effectively a synonym for `run_elab` since `MetaM` lifts to `TermElabM`.) -/ From a52e96408df40f101363ef6d1c9c5e620f67ee95 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sat, 14 Mar 2026 13:56:52 -0700 Subject: [PATCH 02/13] style --- src/Lean/Expr.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 7224cbd0866b..6b3f52c8c542 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -301,8 +301,8 @@ inductive Expr where of a variable in the expression where there is a variable binder above it (i.e. introduced by a `lam`, `forallE`, or `letE`). - The `deBruijnIndex` parameter is the *de-Bruijn* index for the bound - variable. See [the Wikipedia page on de-Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index) + The `deBruijnIndex` parameter is the *de Bruijn* index for the bound + variable. See [the Wikipedia page on de Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index) for additional information. For example, consider the expression `fun x : Nat => forall y : Nat, x = y`. @@ -321,8 +321,8 @@ inductive Expr where | bvar (deBruijnIndex : Nat) /-- - The `fvar` constructor represent free variables. These *free* variable - occurrences are not bound by an earlier `lam`, `forallE`, or `letE` + The `fvar` constructor represent free variables. Such a *free* variable + occurrence is not bound by an earlier `lam`, `forallE`, or `letE` constructor and its binder exists in a local context only. Note that Lean uses the *locally nameless approach*. See [McBride and McKinna](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf) From 1cf24c1a22021ab4fa04a2f325ce41a09b94f195 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sat, 14 Mar 2026 13:57:21 -0700 Subject: [PATCH 03/13] grammar error --- src/Lean/Expr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 6b3f52c8c542..b8ff652d6717 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -321,7 +321,7 @@ inductive Expr where | bvar (deBruijnIndex : Nat) /-- - The `fvar` constructor represent free variables. Such a *free* variable + The `fvar` constructor represents free variables. Such a *free* variable occurrence is not bound by an earlier `lam`, `forallE`, or `letE` constructor and its binder exists in a local context only. From c68a7770c424d03a6e6a7a186de3ac7dd7cacbc9 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sat, 14 Mar 2026 13:57:30 -0700 Subject: [PATCH 04/13] incorrect reference --- src/Lean/Expr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index b8ff652d6717..8d468fabc6b9 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -330,7 +330,7 @@ inductive Expr where When "visiting" the body of a binding expression (i.e. `lam`, `forallE`, or `letE`), bound variables are converted into free variables using a unique identifier, - and their user-facing name, type, value (for `LetE`), and binder annotation + and their user-facing name, type, value (for `letE`), and binder annotation are stored in the `LocalContext`. -/ | fvar (fvarId : FVarId) From 5049e19387037eb4042a1c2704e91588cfc38df8 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sat, 14 Mar 2026 13:57:41 -0700 Subject: [PATCH 05/13] broken link --- src/Lean/Expr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 8d468fabc6b9..eaca0436b346 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -325,7 +325,7 @@ inductive Expr where occurrence is not bound by an earlier `lam`, `forallE`, or `letE` constructor and its binder exists in a local context only. - Note that Lean uses the *locally nameless approach*. See [McBride and McKinna](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf) + Note that Lean uses the *locally nameless approach*. See [McBride and McKinna](https://doi.org/10.1145/1017472.1017477) for additional details. When "visiting" the body of a binding expression (i.e. `lam`, `forallE`, or `letE`), From 3ac539d71fce1b867dab63ad4aa0b4ffc684a699 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sat, 14 Mar 2026 15:16:58 -0700 Subject: [PATCH 06/13] minor error --- src/Lean/Expr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index eaca0436b346..62cc886b9230 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -363,7 +363,7 @@ inductive Expr where A function application. For example, the natural number one, i.e. `Nat.succ Nat.zero` is represented as - ``Expr.app (.const `Nat.succ []) (.const .zero [])``. + ``Expr.app (.const `Nat.succ []) (.const `Nat.zero [])``. Note that multiple arguments are represented using partial application. For example, the two argument application `f x y` is represented as From 10c992daf3b8b2362edf9df8c102cb1048c5e78b Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sat, 14 Mar 2026 15:17:07 -0700 Subject: [PATCH 07/13] grammar error --- src/Lean/Expr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 62cc886b9230..b03c5cea306f 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -383,7 +383,7 @@ inductive Expr where | lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo) /-- - A dependent arrow `(a : α) → β)` (aka forall-expression) where `β` may dependent + A dependent arrow `(a : α) → β)` (aka forall-expression) where `β` may depend on `a`. Note that this constructor is also used to represent non-dependent arrows where `β` does not depend on `a`. From e0ebf619e4db20425ad90065bef144c4fa999547 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sat, 14 Mar 2026 18:02:25 -0700 Subject: [PATCH 08/13] incorrect constant --- src/Init/Data/Array/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 55ad75d8f63c..17bb601808f2 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -559,9 +559,9 @@ def modifyOp (xs : Array α) (idx : Nat) (f : α → α) : Array α := xs.modify idx f /-- - We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime. + We claim this unsafe implementation is correct because an array cannot have more than `USize.size` elements in our runtime. - This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < usizeSz` to true. -/ + This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < USize.size` to true. -/ @[inline] unsafe def forIn'Unsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β := let sz := as.usize let rec @[specialize] loop (i : USize) (b : β) : m β := do From f9d6da3ba938692b7420d24652958029ba0e1819 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sat, 14 Mar 2026 23:55:10 -0700 Subject: [PATCH 09/13] grammar error --- src/Init/Prelude.lean | 2 +- tests/elab/Reparen.lean.out.expected | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 6b33e68b82f3..df1cd7e77fe1 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -4674,7 +4674,7 @@ inductive Name where /-- The "anonymous" name. -/ | anonymous : Name /-- - A string name. The name `Lean.Meta.run` is represented at + A string name. The name `Lean.Meta.run` is represented as ```lean .str (.str (.str .anonymous "Lean") "Meta") "run" ``` diff --git a/tests/elab/Reparen.lean.out.expected b/tests/elab/Reparen.lean.out.expected index f3feac0b4c47..d844206b0206 100644 --- a/tests/elab/Reparen.lean.out.expected +++ b/tests/elab/Reparen.lean.out.expected @@ -4620,7 +4620,7 @@ inductive Name where /-- The "anonymous" name. -/ | anonymous : Name /-- - A string name. The name `Lean.Meta.run` is represented at + A string name. The name `Lean.Meta.run` is represented as ```lean .str (.str (.str .anonymous "Lean") "Meta") "run" ``` From f0bc59aec1ac78203ae338b72ca455d1da5b1389 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sun, 15 Mar 2026 00:02:34 -0700 Subject: [PATCH 10/13] incorrect docstring --- src/Lean/Expr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index b03c5cea306f..9b3a71b39063 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -253,7 +253,7 @@ instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (S instance : Inhabited (FVarIdMap α) where default := {} -/-- Universe metavariable Id -/ +/-- Expression metavariable Id -/ structure MVarId where name : Name deriving Inhabited, BEq, Hashable From 8d3ba456fb597c94e4f6b9886d1df528d403b28c Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sun, 15 Mar 2026 00:30:24 -0700 Subject: [PATCH 11/13] grammar error --- src/Lean/MetavarContext.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 137bfbb085cd..0c95664f5627 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -510,7 +510,7 @@ def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool /-- Add `mvarId := u` to the universe metavariable assignment. - This method does not check whether `mvarId` is already assigned, nor it checks whether + This method does not check whether `mvarId` is already assigned, nor does it check whether a cycle is being introduced. This is a low-level API, and it is safer to use `isLevelDefEq (mkLevelMVar mvarId) u`. -/ @@ -523,7 +523,7 @@ def assignLevelMVarExp (m : MetavarContext) (mvarId : LMVarId) (val : Level) : M /-- Add `mvarId := x` to the metavariable assignment. -This method does not check whether `mvarId` is already assigned, nor it checks whether +This method does not check whether `mvarId` is already assigned, nor does it check whether a cycle is being introduced, or whether the expression has the right type. This is a low-level API, and it is safer to use `isDefEq (mkMVar mvarId) x`. -/ From 8870bdd88be156cf02c3977bfdbc862e656ffd88 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sun, 15 Mar 2026 01:15:01 -0700 Subject: [PATCH 12/13] grammar errors --- src/Lean/Meta/Tactic/Util.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index d085c40a6f81..b583d6d0da51 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -68,11 +68,11 @@ def _root_.Lean.MVarId.checkNotAssigned (mvarId : MVarId) (tacticName : Name) : ++ .note "This likely indicates an internal error in this tactic or a prior one" throwTacticEx tacticName mvarId msg -/-- Get the type the given metavariable. -/ +/-- Get the type of the given metavariable. -/ def _root_.Lean.MVarId.getType (mvarId : MVarId) : MetaM Expr := return (← mvarId.getDecl).type -/-- Get the type the given metavariable after instantiating metavariables and reducing to +/-- Get the type of the given metavariable after instantiating metavariables and reducing to weak head normal form. -/ -- The `instantiateMVars` needs to be on the outside, -- since `whnf` can unfold local definitions which may introduce metavariables. From c7a3522791f9ae28a20e0eab2cc4c3a192f388d3 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sun, 15 Mar 2026 10:51:36 -0700 Subject: [PATCH 13/13] HashMap is not dependent --- src/Std/Data/HashMap/Raw.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index 48b60d460e81..3b6d0d128680 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -16,7 +16,7 @@ set_option autoImplicit false /-! # Hash maps with unbundled well-formedness invariant -This module develops the type `Std.HashMap.Raw` of dependent hash maps with unbundled +This module develops the type `Std.HashMap.Raw` of hash maps with unbundled well-formedness invariant. This version is safe to use in nested inductive types. The well-formedness predicate is