chore: debug mismatch w/ CI lake cache

.claude/CLAUDE.md

@@ -7,6 +7,11 @@ To build Lean you should use `make -j$(nproc) -C build/release`.
 The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
 Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
 
+To rebuild individual modules without a full build, use Lake directly:
+```
+cd src && lake build Init.Prelude
+```
+
 ## Running Tests
 
 See `tests/README.md` for full documentation. Quick reference:
@@ -61,8 +66,6 @@ To rebuild individual stage 2 modules without a full `make stage2`, use Lake dir
 cd build/release/stage2 && lake build Init.Prelude
 ```
 
-To run tests in stage2, replace `-C build/release` from above with `-C build/release/stage2`.
-
 ## New features
 
 When asked to implement new features:

.github/workflows/build-template.yml

@@ -201,6 +201,7 @@ jobs:
         if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
         run: |
           curl --version
+          cat build/stage1/lib/lean/Leanc.trace
           cd src
           time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
           time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}

.github/workflows/ci.yml

@@ -305,8 +305,7 @@ jobs:
                 "test": true,
                 "CMAKE_PRESET": "reldebug",
                 // * `elab_bench/big_do` crashes with exit code 134
-                // * `compile_bench/channel` randomly segfaults
-                "CTEST_OPTIONS": "-E 'elab_bench/big_do|compile_bench/channel'",
+                "CTEST_OPTIONS": "-E 'elab_bench/big_do'",
               },
               {
                 "name": "Linux fsanitize",

CMakeLists.txt

@@ -129,7 +129,6 @@ if(USE_MIMALLOC)
     # cadical, it might be worth reorganizing the directory structure.
     SOURCE_DIR
     "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
-    EXCLUDE_FROM_ALL
   )
   FetchContent_MakeAvailable(mimalloc)
 endif()
@@ -221,9 +220,7 @@ add_custom_target(
   DEPENDS stage2
 )
 
-add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1-configure)
-
-add_custom_target(cache-get COMMAND $(MAKE) -C stage1 cache-get DEPENDS stage1-configure)
+add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1)
 
 install(CODE "execute_process(COMMAND make -C stage1 install)")
 

src/CMakeLists.txt

@@ -110,7 +110,6 @@ option(RUNTIME_STATS "RUNTIME_STATS" OFF)
 option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
 option(USE_GMP "USE_GMP" ON)
 option(USE_MIMALLOC "use mimalloc" ON)
-set(LEAN_MI_SECURE 0 CACHE STRING "Configure mimalloc memory safety mitigations (https://github.com/microsoft/mimalloc/blob/v2.2.7/include/mimalloc/types.h#L56-L60)")
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
@@ -118,7 +117,6 @@ option(USE_LAKE "Use Lake instead of lean.mk for building core libs from languag
 option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
 set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
-set(LEAN_EXTRA_LAKE_OPTS "" CACHE STRING "extra options to lake")
 set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
@@ -128,7 +126,7 @@ string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
 # option used by the CI to fail on warnings
 option(WFAIL "Fail build if warnings are emitted by Lean" ON)
 if(WFAIL MATCHES "ON")
-  string(APPEND LEAN_EXTRA_LAKE_OPTS " --wfail")
+  string(APPEND LAKE_EXTRA_ARGS " --wfail")
   string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
 endif()
 
@@ -994,13 +992,6 @@ add_custom_target(
 
 add_custom_target(clean-olean DEPENDS clean-stdlib)
 
-if(USE_LAKE_CACHE)
-  add_custom_target(
-    cache-get
-    COMMAND ${PREV_STAGE}/bin/lake${CMAKE_EXECUTABLE_SUFFIX} cache get --repo=leanprover/lean4
-  )
-endif()
-
 install(
   DIRECTORY "${CMAKE_BINARY_DIR}/lib/"
   DESTINATION lib

src/Init/Data/Array/Basic.lean

@@ -802,7 +802,6 @@ Examples:
 def firstM {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) : m β :=
   go 0
 where
-  @[specialize]
   go (i : Nat) : m β :=
     if hlt : i < as.size then
       f as[i] <|> go (i+1)
@@ -1265,7 +1264,7 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec @[specialize] loop (j : Nat) :=
+  let rec loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none

src/Init/Data/Array/Lemmas.lean

@@ -3096,13 +3096,13 @@ theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Array α} {start stop :
 theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Array α} {start stop : Nat} :
     xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
-theorem foldl_eq_foldl_extract {xs : Array α} {f : β → α → β} {init : β} :
+public theorem foldl_eq_foldl_extract {xs : Array α} {f : β → α → β} {init : β} :
     xs.foldl (init := init) (start := start) (stop := stop) f =
       (xs.extract start stop).foldl (init := init) f := by
   simp only [foldl_eq_foldlM]
   rw [foldlM_start_stop]
 
-theorem foldr_eq_foldr_extract {xs : Array α} {f : α → β → β} {init : β} :
+public theorem foldr_eq_foldr_extract {xs : Array α} {f : α → β → β} {init : β} :
     xs.foldr (init := init) (start := start) (stop := stop) f =
       (xs.extract stop start).foldr (init := init) f := by
   simp only [foldr_eq_foldrM]

src/Init/Data/Array/QSort/Basic.lean

@@ -33,7 +33,6 @@ if necessary so that the middle (pivot) element is at index `hi`.
 We then iterate from `k = lo` to `k = hi`, with a pointer `i` starting at `lo`, and
 swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
 -/
-@[inline]
 def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w : lo ≤ hi := by omega)
     (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m ≤ hi} × Vector α n :=
   let mid := (lo + hi) / 2
@@ -45,7 +44,7 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w
   -- elements in `[i, k)` are greater than or equal to `pivot`,
   -- elements in `[k, hi)` are unexamined,
   -- while `as[hi]` is (by definition) the pivot.
-  let rec @[specialize] loop (as : Vector α n) (i k : Nat)
+  let rec loop (as : Vector α n) (i k : Nat)
       (ilo : lo ≤ i := by omega) (ik : i ≤ k := by omega) (w : k ≤ hi := by omega) :=
     if h : k < hi then
       if lt as[k] pivot then

src/Init/Data/Array/Subarray.lean

@@ -80,7 +80,7 @@ instance : SliceSize (Internal.SubarrayData α) where
   size s := s.internalRepresentation.stop - s.internalRepresentation.start
 
 @[grind =, suggest_for Subarray.size]
-theorem size_eq {xs : Subarray α} :
+public theorem size_eq {xs : Subarray α} :
     xs.size = xs.stop - xs.start := by
   simp [Std.Slice.size, SliceSize.size, start, stop]
 

src/Init/Data/Int/Compare.lean

@@ -74,7 +74,7 @@ protected theorem isGE_compare {a b : Int} :
   rw [← Int.compare_swap, Ordering.isGE_swap]
   exact Int.isLE_compare
 
-instance : Std.LawfulOrderOrd Int where
+public instance : Std.LawfulOrderOrd Int where
   isLE_compare _ _ := Int.isLE_compare
   isGE_compare _ _ := Int.isGE_compare
 

src/Init/Data/Iterators/Basic.lean

@@ -42,29 +42,29 @@ The conversion functions {name (scope := "Init.Data.Iterators.Basic")}`Shrink.de
 {name (scope := "Init.Data.Iterators.Basic")}`Shrink.inflate` form an equivalence between
 {name}`α` and {lean}`Shrink α`, but this equivalence is intentionally not definitional.
 -/
-def Shrink (α : Type u) : Type u := Internal.idOpaque.1 α
+public def Shrink (α : Type u) : Type u := Internal.idOpaque.1 α
 
 /-- Converts elements of {name}`α` into elements of {lean}`Shrink α`. -/
 @[always_inline]
-def Shrink.deflate {α} (x : α) : Shrink α :=
+public def Shrink.deflate {α} (x : α) : Shrink α :=
   cast (by simp [Shrink, Internal.idOpaque.property]) x
 
 /-- Converts elements of {lean}`Shrink α` into elements of {name}`α`. -/
 @[always_inline]
-def Shrink.inflate {α} (x : Shrink α) : α :=
+public def Shrink.inflate {α} (x : Shrink α) : α :=
   cast (by simp [Shrink, Internal.idOpaque.property]) x
 
 @[simp, grind =]
-theorem Shrink.deflate_inflate {α} {x : Shrink α} :
+public theorem Shrink.deflate_inflate {α} {x : Shrink α} :
     Shrink.deflate x.inflate = x := by
   simp [deflate, inflate]
 
 @[simp, grind =]
-theorem Shrink.inflate_deflate {α} {x : α} :
+public theorem Shrink.inflate_deflate {α} {x : α} :
     (Shrink.deflate x).inflate = x := by
   simp [deflate, inflate]
 
-theorem Shrink.inflate_inj {α} {x y : Shrink α} :
+public theorem Shrink.inflate_inj {α} {x y : Shrink α} :
     x.inflate = y.inflate ↔ x = y := by
   apply Iff.intro
   · intro h
@@ -72,7 +72,7 @@ theorem Shrink.inflate_inj {α} {x y : Shrink α} :
   · rintro rfl
     rfl
 
-theorem Shrink.deflate_inj {α} {x y : α} :
+public theorem Shrink.deflate_inj {α} {x y : α} :
     Shrink.deflate x = Shrink.deflate y ↔ x = y := by
   apply Iff.intro
   · intro h

src/Init/Data/Iterators/Combinators/Monadic/Append.lean

@@ -190,7 +190,7 @@ def Append.instFinitenessRelation [Monad m] [Iterator α₁ m β] [Iterator α
       exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
 
 @[no_expose]
-instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+public instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
     [Finite α₁ m] [Finite α₂ m] : Finite (Append α₁ α₂ m β) m :=
   .of_finitenessRelation instFinitenessRelation
 

src/Init/Data/List/Basic.lean

@@ -282,7 +282,6 @@ The lexicographic order with respect to `lt` is:
 * `as.lex [] = false` is `false`
 * `(a :: as).lex (b :: bs)` is true if `lt a b` or `a == b` and `lex lt as bs` is true.
 -/
-@[specialize]
 def lex [BEq α] (l₁ l₂ : List α) (lt : α → α → Bool := by exact (· < ·)) : Bool :=
   match l₁, l₂ with
   | [],      _ :: _  => true
@@ -1005,7 +1004,6 @@ Examples:
  * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [8, 3, 2, 4, 2, 7, 4]`
  * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 100) = []`
 -/
-@[specialize]
 def dropWhile (p : α → Bool) : List α → List α
   | []   => []
   | a::l => match p a with
@@ -1462,11 +1460,9 @@ Examples:
 ["circle", "square", "triangle"]
 ```
 -/
-@[inline]
 def modifyTailIdx (l : List α) (i : Nat) (f : List α → List α) : List α :=
   go i l
 where
-  @[specialize]
   go : Nat → List α → List α
   | 0, l => f l
   | _+1, [] => []
@@ -1502,7 +1498,6 @@ Examples:
  * `[1, 2, 3].modify 2 (· * 10) = [1, 2, 30]`
  * `[1, 2, 3].modify 3 (· * 10) = [1, 2, 3]`
 -/
-@[inline]
 def modify (l : List α) (i : Nat) (f : α → α) : List α :=
   l.modifyTailIdx i (modifyHead f)
 
@@ -1609,7 +1604,6 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1`
 * `[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none`
 -/
-@[specialize]
 def find? (p : α → Bool) : List α → Option α
   | []    => none
   | a::as => match p a with
@@ -1632,7 +1626,6 @@ Examples:
  * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
  * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
-@[specialize]
 def findSome? (f : α → Option β) : List α → Option β
   | []    => none
   | a::as => match f a with
@@ -1656,7 +1649,6 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 5) = some 2`
 * `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 1) = none`
 -/
-@[specialize]
 def findRev? (p : α → Bool) : List α → Option α
   | []    => none
   | a::as => match findRev? p as with
@@ -1675,7 +1667,6 @@ Examples:
  * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 5 then some (10 * x) else none) = some 20`
  * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
-@[specialize]
 def findSomeRev? (f : α → Option β) : List α → Option β
   | []    => none
   | a::as => match findSomeRev? f as with
@@ -1726,11 +1717,9 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4`
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none`
 -/
-@[inline]
 def findIdx? (p : α → Bool) (l : List α) : Option Nat :=
   go l 0
 where
-  @[specialize]
   go : List α → Nat → Option Nat
   | [], _ => none
   | a :: l, i => if p a then some i else go l (i + 1)
@@ -1761,7 +1750,6 @@ Examples:
 @[inline] def findFinIdx? (p : α → Bool) (l : List α) : Option (Fin l.length) :=
   go l 0 (by simp)
 where
-  @[specialize]
   go : (l' : List α) → (i : Nat) → (h : l'.length + i = l.length) → Option (Fin l.length)
   | [], _, _ => none
   | a :: l, i, h =>
@@ -1898,7 +1886,7 @@ Examples:
 * `[2, 4, 5, 6].any (· % 2 = 0) = true`
 * `[2, 4, 5, 6].any (· % 2 = 1) = true`
 -/
-@[suggest_for List.some, specialize]
+@[suggest_for List.some]
 def any : (l : List α) → (p : α → Bool) → Bool
   | [], _ => false
   | h :: t, p => p h || any t p
@@ -1918,7 +1906,7 @@ Examples:
 * `[2, 4, 6].all (· % 2 = 0) = true`
 * `[2, 4, 5, 6].all (· % 2 = 0) = false`
 -/
-@[suggest_for List.every, specialize]
+@[suggest_for List.every]
 def all : List α → (α → Bool) → Bool
   | [], _ => true
   | h :: t, p => p h && all t p
@@ -2019,7 +2007,6 @@ Examples:
 * `[1, 2, 3].zipWithAll Prod.mk [5, 6] = [(some 1, some 5), (some 2, some 6), (some 3, none)]`
 * `[x₁, x₂].zipWithAll f [y] = [f (some x₁) (some y), f (some x₂) none]`
 -/
-@[specialize]
 def zipWithAll (f : Option α → Option β → γ) : List α → List β → List γ
   | [], bs => bs.map fun b => f none (some b)
   | a :: as, [] => (a :: as).map fun a => f (some a) none

src/Init/Data/List/Control.lean

@@ -444,8 +444,8 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
     intro b
     cases b <;> simp
 
-@[inline, expose] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : @& List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop : (as' : @& List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
+@[inline, expose] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
     | [], b, _    => pure b
     | a::as', b, h => do
       have : a ∈ as := by

src/Init/Data/List/MinMax.lean

@@ -37,7 +37,7 @@ open Nat
 @[simp, grind =] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl
 
 @[simp, grind =]
-theorem min?_singleton [Min α] {x : α} : [x].min? = some x :=
+public theorem min?_singleton [Min α] {x : α} : [x].min? = some x :=
   (rfl)
 
 -- We don't put `@[simp]` on `min?_cons'`,
@@ -52,7 +52,7 @@ theorem min?_cons' [Min α] {xs : List α} : (x :: xs).min? = some (foldl min x
   cases xs <;> simp [min?]
 
 @[simp, grind =]
-theorem isSome_min?_iff [Min α] {xs : List α} : xs.min?.isSome ↔ xs ≠ [] := by
+public theorem isSome_min?_iff [Min α] {xs : List α} : xs.min?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [min?]
 
 @[grind .]
@@ -247,7 +247,7 @@ theorem foldl_min_eq_min [Min α] [Std.IdempotentOp (min : α → α → α)] [S
 @[simp, grind =] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
 
 @[simp, grind =]
-theorem max?_singleton [Max α] {x : α} : [x].max? = some x :=
+public theorem max?_singleton [Max α] {x : α} : [x].max? = some x :=
   (rfl)
 
 -- We don't put `@[simp]` on `max?_cons'`,
@@ -262,7 +262,7 @@ theorem max?_cons' [Max α] {xs : List α} : (x :: xs).max? = some (foldl max x
   cases xs <;> simp [max?]
 
 @[simp, grind =]
-theorem isSome_max?_iff [Max α] {xs : List α} : xs.max?.isSome ↔ xs ≠ [] := by
+public theorem isSome_max?_iff [Max α] {xs : List α} : xs.max?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [max?]
 
 @[grind .]

src/Init/Data/Nat/Compare.lean

@@ -70,7 +70,7 @@ protected theorem isGE_compare {a b : Nat} :
   rw [← Nat.compare_swap, Ordering.isGE_swap]
   exact Nat.isLE_compare
 
-instance : Std.LawfulOrderOrd Nat where
+public instance : Std.LawfulOrderOrd Nat where
   isLE_compare _ _ := Nat.isLE_compare
   isGE_compare _ _ := Nat.isGE_compare
 

src/Init/Data/Nat/Gcd.lean

@@ -60,7 +60,7 @@ theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x := by
   cases n with
   | zero => simp
   | succ n =>
-    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `(rfl)` instead
+    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead
     rw [gcd_succ]
     exact gcd_zero_left _
 instance : Std.LawfulIdentity gcd 0 where

src/Init/Data/Option/Attach.lean

@@ -444,7 +444,7 @@ instance : MonadAttach Option where
   CanReturn x a := x = some a
   attach x := x.attach
 
-instance : LawfulMonadAttach Option where
+public instance : LawfulMonadAttach Option where
   map_attach {α} x := by simp [MonadAttach.attach]
   canReturn_map_imp {α P x a} := by
     cases x
@@ -455,7 +455,7 @@ end Option
 
 namespace OptionT
 
-instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
+public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (OptionT m) where
   map_attach {α} x := by
     apply OptionT.ext
@@ -466,7 +466,7 @@ instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     | ⟨some a, _⟩ => simp [OptionT.pure, OptionT.mk]
     | ⟨none, _⟩ => simp
 
-instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
+public instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
     LawfulMonadAttach (OptionT m) where
   canReturn_map_imp {α P x a} h := by
     simp only [MonadAttach.CanReturn, OptionT.run_map] at h

src/Init/Data/Order/LemmasExtra.lean

@@ -152,7 +152,7 @@ public theorem max_eq_if_isGE_compare {α : Type u} [Ord α] [LE α] {_ : Max α
     {a b : α} : max a b = if (compare a b).isGE then a else b := by
   open Classical in simp [max_eq_if, isGE_compare]
 
-theorem min_le_min [LE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [IsLinearOrder α] (a b : α) : min a b ≤ min b a := by
+private theorem min_le_min [LE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [IsLinearOrder α] (a b : α) : min a b ≤ min b a := by
   apply (LawfulOrderInf.le_min_iff (min a b) b a).2
   rw [And.comm]
   by_cases h : a ≤ b

src/Init/Data/Range/Polymorphic/NatLemmas.lean

@@ -1718,7 +1718,7 @@ theorem toArray_roc_append_toArray_roc {l m n : Nat} (h : l ≤ m) (h' : m ≤ n
 @[simp]
 theorem getElem_toArray_roc {m n i : Nat} (_h : i < (m<...=n).toArray.size) :
     (m<...=n).toArray[i]'_h = m + 1 + i := by
-  simp [toArray_roc_eq_toArray_rco]
+simp [toArray_roc_eq_toArray_rco]
 
 theorem getElem?_toArray_roc {m n i : Nat} :
     (m<...=n).toArray[i]? = if i < n - m then some (m + 1 + i) else none := by

src/Init/Data/Range/Polymorphic/SInt.lean

@@ -248,11 +248,11 @@ instance : HasModel Int8 (BitVec 8) where
   le_iff_encode_le := by simp [LE.le, Int8.le]
   lt_iff_encode_lt := by simp [LT.lt, Int8.lt]
 
-theorem succ?_eq_minValueSealed {x : Int8} :
+private theorem succ?_eq_minValueSealed {x : Int8} :
     UpwardEnumerable.succ? x = if x + 1 = minValueSealed then none else some (x + 1) :=
   (rfl)
 
-theorem succMany?_eq_maxValueSealed {i : Int8} :
+private theorem succMany?_eq_maxValueSealed {i : Int8} :
     UpwardEnumerable.succMany? n i =
       have := i.minValue_le_toInt
       if h : i.toInt + n ≤ maxValueSealed.toInt then some (.ofIntLE _ (by omega) (maxValueSealed_def ▸ h)) else none :=
@@ -605,12 +605,12 @@ theorem minValueSealed_def : minValueSealed = ISize.minValue := (rfl)
 theorem maxValueSealed_def : maxValueSealed = ISize.maxValue := (rfl)
 seal minValueSealed maxValueSealed
 
-theorem toBitVec_minValueSealed_eq_intMinSealed :
+private theorem toBitVec_minValueSealed_eq_intMinSealed :
     minValueSealed.toBitVec = BitVec.Signed.intMinSealed System.Platform.numBits := by
   rw [minValueSealed_def, BitVec.Signed.intMinSealed_def, toBitVec_minValue]
   have := System.Platform.numBits_eq; generalize System.Platform.numBits = a at this ⊢
   rcases this with rfl | rfl <;> rfl
-theorem toBitVec_maxValueSealed_eq_intMaxSealed :
+private theorem toBitVec_maxValueSealed_eq_intMaxSealed :
     maxValueSealed.toBitVec = BitVec.Signed.intMaxSealed System.Platform.numBits := by
   rw [maxValueSealed_def, BitVec.Signed.intMaxSealed_def, toBitVec_maxValue]
   have := System.Platform.numBits_eq; generalize System.Platform.numBits = a at this ⊢

src/Init/Data/Slice/Array/Lemmas.lean

@@ -233,7 +233,7 @@ public theorem Subarray.toList_eq {xs : Subarray α} :
   simp [this, ListSlice.toList_eq, lslice]
 
 -- TODO: The current `List.extract_eq_drop_take` should be called `List.extract_eq_take_drop`
-theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start stop : Nat} :
+private theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start stop : Nat} :
     l.extract start stop = (l.take stop).drop start := by
   simp [List.take_drop]
   by_cases start ≤ stop

src/Init/Data/String/Decode.lean

@@ -94,7 +94,7 @@ public def String.utf8EncodeCharFast (c : Char) : List UInt8 :=
      (v >>>  6).toUInt8 &&& 0x3f ||| 0x80,
               v.toUInt8 &&& 0x3f ||| 0x80]
 
-theorem Nat.add_two_pow_eq_or_of_lt {b : Nat} (i : Nat) (b_lt : b < 2 ^ i) (a : Nat) :
+private theorem Nat.add_two_pow_eq_or_of_lt {b : Nat} (i : Nat) (b_lt : b < 2 ^ i) (a : Nat) :
     b + 2 ^ i * a = b ||| 2 ^ i * a := by
   rw [Nat.add_comm, Nat.or_comm, Nat.two_pow_add_eq_or_of_lt b_lt]
 

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Basic.lean

@@ -909,7 +909,7 @@ theorem Slice.Pos.skipWhile_copy {ρ : Type} {pat : ρ} [ForwardPattern pat] [Pa
   simp
 
 @[simp]
-theorem Pos.le_skipWhile {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
+theorem Pos.skipWhile_le {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
     [LawfulForwardPatternModel pat] {s : String} {pos : s.Pos} : pos ≤ pos.skipWhile pat := by
   simp [skipWhile_eq_skipWhile_toSlice, Pos.le_ofToSlice_iff]
 

src/Init/Grind/Ring/Basic.lean

@@ -564,28 +564,6 @@ end Ring
 
 end IsCharP
 
-/--
-`PowIdentity α p` states that `x ^ p = x` holds for all elements of `α`.
-
-The primary source of instances is Fermat's little theorem: for a finite field with `q` elements,
-`x ^ q = x` for every `x`. For `Fin p` or `ZMod p` with prime `p`, this gives `x ^ p = x`.
-
-The `grind` ring solver uses this typeclass to add the relation `x ^ p - x = 0` to the
-Groebner basis, which allows it to reduce high-degree polynomials. Mathlib can provide
-instances for general finite fields via `FiniteField.pow_card`.
--/
-class PowIdentity (α : Type u) [CommSemiring α] (p : outParam Nat) : Prop where
-  /-- Every element satisfies `x ^ p = x`. -/
-  pow_eq (x : α) : x ^ p = x
-
-namespace PowIdentity
-
-variable [CommSemiring α] [PowIdentity α p]
-
-theorem pow (x : α) : x ^ p = x := pow_eq x
-
-end PowIdentity
-
 open AddCommGroup
 
 theorem no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α] {k : Int} {a : α}

src/Init/Grind/Ring/Envelope.lean

@@ -193,7 +193,7 @@ theorem mul_assoc (a b c : Q α) : mul (mul a b) c = mul a (mul b c) := by
   simp [Semiring.left_distrib, Semiring.right_distrib]; refine ⟨0, ?_⟩; ac_rfl
 
 theorem mul_one (a : Q α) : mul a (natCast 1) = a := by
-  obtain ⟨⟨_, _⟩⟩ := a; simp
+obtain ⟨⟨_, _⟩⟩ := a; simp
 
 theorem one_mul (a : Q α) : mul (natCast 1) a = a := by
   obtain ⟨⟨_, _⟩⟩ := a; simp

src/Init/GrindInstances/Ring/Fin.lean

@@ -156,12 +156,6 @@ instance [i : NeZero n] : ToInt.Pow (Fin n) (.co 0 n) where
       rw [pow_succ, ToInt.Mul.toInt_mul, ih, ← ToInt.wrap_toInt,
         ← IntInterval.wrap_mul (by simp), Int.pow_succ, ToInt.wrap_toInt]
 
-instance : PowIdentity (Fin 2) 2 where
-  pow_eq x := by
-    match x with
-    | ⟨0, _⟩ => rfl
-    | ⟨1, _⟩ => rfl
-
 end Fin
 
 end Lean.Grind

src/Init/Internal/Order.lean

@@ -7,7 +7,5 @@ module
 
 prelude
 public import Init.Internal.Order.Basic
-public import Init.Internal.Order.ExtrinsicFix
 public import Init.Internal.Order.Lemmas
-public import Init.Internal.Order.MonadTail
 public import Init.Internal.Order.Tactic

src/Init/Internal/Order/ExtrinsicFix.lean

@@ -1,117 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf, Robin Arnez
--/
-module
-
-prelude
-public import Init.Internal.Order.Basic
-public import Init.Internal.Order.MonadTail
-import Init.Classical
-
-set_option linter.missingDocs true
-
-/-!
-This module provides a fixpoint combinator that combines advantages of `partial` and
-`partial_fixpoint` recursion.
-
-The combinator is similar to {lean}`CCPO.fix`, but does not require a CCPO instance or
-monotonicity proof at the definition site. Therefore, it can be used in situations in which
-these constraints are unavailable (e.g., when the monad does not have a `MonadTail` instance).
-Given a CCPO and monotonicity proof, there are theorems guaranteeing that it equals
-{lean}`CCPO.fix` and satisfies fixpoint induction.
--/
-
-public section
-
-namespace Lean.Order
-
-/--
-The function implemented as the loop {lean}`opaqueFix f = f (opaqueFix f)`.
-{lean}`opaqueFix f` is the fixpoint of {name}`f`, as long as `f` is monotone with respect to
-some CCPO on `α`.
-
-The loop might run forever depending on {name}`f`. It is opaque, i.e., it is impossible to prove
-nontrivial properties about it.
--/
-@[specialize]
-partial def opaqueFix {α : Sort u} [Nonempty α] (f : α → α) : α :=
-  f (opaqueFix f)
-
-/-
-SAFE assuming that the code generated by iteration over `f` is equivalent to the CCPO
-fixpoint of `f` if there exists a CCPO making `f` monotone.
--/
-open _root_.Classical in
-/--
-A fixpoint combinator that can be used to construct recursive definitions with an *extrinsic*
-proof of monotonicity.
-
-Given a fixpoint functional {name}`f`, {lean}`extrinsicFix f` is the recursive function obtained
-by having {name}`f` call itself recursively.
-
-If there is no CCPO on `α` making {name}`f` monotone, {lean}`extrinsicFix f` might run forever.
-In this case, nothing interesting can be proved about the result; it is opaque.
-
-If there _is_ a CCPO on `α` making {name}`f` monotone, {lean}`extrinsicFix f` is equivalent to
-{lean}`CCPO.fix f`, logically and regarding its termination behavior.
--/
-@[cbv_opaque, implemented_by opaqueFix]
-def extrinsicFix {α : Sort u} [Nonempty α] (f : α → α) : α :=
-  if h : ∃ x, x = f x then
-    h.choose
-  else
-    -- Return `opaqueFix f` so that `implemented_by opaqueFix` is sound.
-    -- In effect, `extrinsicFix` is opaque if no fixpoint exists.
-    opaqueFix f
-
-/--
-A fixpoint combinator that allows for deferred proofs of monotonicity.
-
-{lean}`extrinsicFix f` is a function implemented as the loop
-{lean}`extrinsicFix f = f (extrinsicFix f)`.
-
-If there is a CCPO making `f` monotone, {name}`extrinsicFix_eq` proves that it satisfies the
-fixpoint equation, and {name}`extrinsicFix_induct` enables fixpoint induction.
-Otherwise, {lean}`extrinsicFix f` is opaque, i.e., it is impossible to prove nontrivial
-properties about it.
--/
-add_decl_doc extrinsicFix
-
-/-- Every CCPO has at least one element (the bottom element). -/
-noncomputable local instance CCPO.instNonempty [CCPO α] : Nonempty α := ⟨bot⟩
-
-/--
-The fixpoint equation for `extrinsicFix`: given a proof that the fixpoint exists, unfold
-`extrinsicFix`.
--/
-theorem extrinsicFix_eq {f : α → α}
-    (x : α) (h : x = f x) :
-    letI : Nonempty α := ⟨x⟩; extrinsicFix f = f (extrinsicFix f) := by
-  letI : Nonempty α := ⟨x⟩
-  have h : ∃ x, x = f x := ⟨x, h⟩
-  simp only [extrinsicFix, dif_pos h]
-  exact h.choose_spec
-
-/--
-The fixpoint equation for `extrinsicFix`: given a CCPO instance and monotonicity of `f`,
-{lean}`extrinsicFix f = f (extrinsicFix f)`.
--/
-theorem extrinsicFix_eq_mono [inst : CCPO α] {f : α → α}
-    (hf : monotone f) :
-    extrinsicFix f = f (extrinsicFix f) :=
-  extrinsicFix_eq (fix f hf) (fix_eq hf)
-
-abbrev discardR {C : α → Sort _} {R : α → α → Prop}
-    (f : ∀ a, (∀ a', R a' a → C a') → C a) : ((∀ a, C a) → (∀ a, C a)) :=
-  fun rec a => f a (fun a _ => rec a)
-
-theorem extrinsicFix_eq_wf {C : α → Sort _} [∀ a, Nonempty (C a)] {R : α → α → Prop}
-    {f : ∀ a, (∀ a', R a' a → C a') → C a} (h : WellFounded R) {a : α} :
-    extrinsicFix (discardR f) a = f a (fun a _ => extrinsicFix (discardR f) a) := by
-  suffices extrinsicFix (discardR f) = fun a => f a (fun a _ => extrinsicFix (discardR f) a) by
-    conv => lhs; rw [this]
-  apply extrinsicFix_eq (fun a => WellFounded.fix h f a) (funext fun a => (WellFounded.fix_eq h f a))
-
-end Lean.Order

src/Init/Internal/Order/MonadTail.lean

@@ -1,140 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Init.Internal.Order.Basic
-import all Init.System.ST  -- for EST.bind in MonadTail instance
-
-set_option linter.missingDocs true
-
-public section
-
-namespace Lean.Order
-
-/--
-A *tail monad* is a monad whose bind operation preserves any suitable ordering of the continuation.
-Specifically, `MonadTail m` asserts that every `m β` carries a chain-complete partial order (CCPO)
-and that `>>=` is monotone in its second (continuation) argument with respect to that order.
-
-This is a weaker requirement than `MonoBind`, which requires monotonicity in both arguments.
-`MonadTail` is sufficient for `partial_fixpoint`-based recursive definitions where the
-recursive call only appears in the continuation (second argument) of `>>=`.
--/
-class MonadTail (m : Type u → Type v) [Bind m] where
-  /-- Every `m β` with `Nonempty β` has a chain-complete partial order. -/
-  instCCPO β [Nonempty β] : CCPO (m β)
-  /-- Bind is monotone in the second (continuation) argument. -/
-  bind_mono_right {a : m α} {f₁ f₂ : α → m β} [Nonempty β] (h : ∀ x, f₁ x ⊑ f₂ x) :
-    a >>= f₁ ⊑ a >>= f₂
-
-attribute [implicit_reducible] MonadTail.instCCPO
-attribute [instance] MonadTail.instCCPO
-
-@[scoped partial_fixpoint_monotone]
-theorem MonadTail.monotone_bind_right
-    (m : Type u → Type v) [Monad m] [MonadTail m]
-    {α β : Type u} [Nonempty β]
-    {γ : Sort w} [PartialOrder γ]
-    (f : m α) (g : γ → α → m β)
-    (hmono : monotone g) :
-    monotone (fun (x : γ) => f >>= g x) :=
-  fun _ _ h => MonadTail.bind_mono_right (hmono _ _ h)
-
-instance : MonadTail Id where
-  instCCPO _ := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
-  bind_mono_right h := h _
-
-instance {σ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] [Nonempty σ] :
-    MonadTail (StateT σ m) where
-  instCCPO α := inferInstanceAs (CCPO (σ → m (α × σ)))
-  bind_mono_right h := by
-    intro s
-    show StateT.bind _ _ s ⊑ StateT.bind _ _ s
-    simp only [StateT.bind]
-    apply MonadTail.bind_mono_right (m := m)
-    intro ⟨x, s'⟩
-    exact h x s'
-
-instance {ε : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
-    MonadTail (ExceptT ε m) where
-  instCCPO β := MonadTail.instCCPO (Except ε β)
-  bind_mono_right h := by
-    apply MonadTail.bind_mono_right (m := m)
-    intro x
-    cases x with
-    | error => exact PartialOrder.rel_refl
-    | ok a => exact h a
-
-instance : MonadTail (Except ε) where
-  instCCPO β := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
-  bind_mono_right h := by
-    cases ‹Except _ _› with
-    | error => exact FlatOrder.rel.refl
-    | ok a => exact h a
-
-instance {m : Type u → Type v} [Monad m] [MonadTail m] :
-    MonadTail (OptionT m) where
-  instCCPO β := MonadTail.instCCPO (Option β)
-  bind_mono_right h := by
-    apply MonadTail.bind_mono_right (m := m)
-    intro x
-    cases x with
-    | none => exact PartialOrder.rel_refl
-    | some a => exact h a
-
-instance : MonadTail Option where
-  instCCPO _ := inferInstance
-  bind_mono_right h := MonoBind.bind_mono_right h
-
-instance {ρ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
-    MonadTail (ReaderT ρ m) where
-  instCCPO α := inferInstanceAs (CCPO (ρ → m α))
-  bind_mono_right h := by
-    intro r
-    show ReaderT.bind _ _ r ⊑ ReaderT.bind _ _ r
-    simp only [ReaderT.bind]
-    apply MonadTail.bind_mono_right (m := m)
-    intro x
-    exact h x r
-
-set_option linter.missingDocs false in
-noncomputable def ST.bot' [Nonempty α] (s : Void σ) : @FlatOrder (ST.Out σ α) (.mk Classical.ofNonempty (Classical.choice ⟨s⟩)) :=
-  .mk Classical.ofNonempty (Classical.choice ⟨s⟩)
-
-instance [Nonempty α] : CCPO (ST σ α) where
-  rel := PartialOrder.rel (α := ∀ s, FlatOrder (ST.bot' s))
-  rel_refl := PartialOrder.rel_refl
-  rel_antisymm := PartialOrder.rel_antisymm
-  rel_trans := PartialOrder.rel_trans
-  has_csup hchain := CCPO.has_csup (α := ∀ s, FlatOrder (ST.bot' s)) hchain
-
-instance : MonadTail (ST σ) where
-  instCCPO _ := inferInstance
-  bind_mono_right {_ _ a f₁ f₂} _ h := by
-    intro w
-    change FlatOrder.rel (ST.bind a f₁ w) (ST.bind a f₂ w)
-    simp only [ST.bind]
-    apply h
-
-instance : MonadTail BaseIO :=
-  inferInstanceAs (MonadTail (ST IO.RealWorld))
-
-instance [Nonempty ε] : MonadTail (EST ε σ) where
-  instCCPO _ := inferInstance
-  bind_mono_right h := MonoBind.bind_mono_right h
-
-instance [Nonempty ε] : MonadTail (EIO ε) :=
-  inferInstanceAs (MonadTail (EST ε IO.RealWorld))
-
-instance : MonadTail IO :=
-  inferInstanceAs (MonadTail (EIO IO.Error))
-
-instance {ω : Type} {σ : Type} {m : Type → Type} [Monad m] [MonadTail m] :
-    MonadTail (StateRefT' ω σ m) :=
-  inferInstanceAs (MonadTail (ReaderT (ST.Ref ω σ) m))
-
-end Lean.Order

src/Init/While.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Core
-public import Init.Internal.Order.ExtrinsicFix
 
 public section
 
@@ -22,38 +21,18 @@ namespace Lean
 inductive Loop where
   | mk
 
-open Lean.Order in
 @[inline]
-def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m]
-    (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
-  haveI : Nonempty (β → m β) := ⟨fun b => pure b⟩
-  Lean.Order.extrinsicFix (fun (cont : β → m β) (b : β) => do
+partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop (b : β) : m β := do
     match ← f () b with
-    | .done val => pure val
-    | .yield val => cont val) init
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop b
+  loop init
 
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
-open Lean.Order in
-theorem Loop.forIn_eq [Monad m] [MonadTail m]
-    {l : Loop} {b : β} {f : Unit → β → m (ForInStep β)} :
-    Loop.forIn l b f = (do
-      match ← f () b with
-      | .done val => pure val
-      | .yield val => Loop.forIn l val f) := by
-  haveI : Nonempty β := ⟨b⟩
-  simp only [Loop.forIn]
-  apply congrFun
-  apply extrinsicFix_eq
-  intro cont₁ cont₂ h b'
-  apply MonadTail.bind_mono_right
-  intro r
-  cases r with
-  | done => exact PartialOrder.rel_refl
-  | yield val => exact h val
-
-syntax (name := doRepeat) "repeat " doSeq : doElem
+syntax "repeat " doSeq : doElem
 
 macro_rules
   | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)

src/Lean/AddDecl.lean

@@ -9,7 +9,6 @@ prelude
 public import Lean.Meta.Sorry
 public import Lean.Util.CollectAxioms
 public import Lean.OriginalConstKind
-import Lean.Compiler.MetaAttr
 import all Lean.OriginalConstKind  -- for accessing `privateConstKindsExt`
 
 public section
@@ -209,12 +208,8 @@ where
       catch _ => pure ()
 
 
-def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true)
-    (markMeta : Bool := false) : CoreM Unit := do
+def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true) : CoreM Unit := do
   addDecl decl
-  if markMeta then
-    for n in decl.getNames do
-      modifyEnv (Lean.markMeta · n)
   compileDecl decl (logErrors := logCompileErrors)
 
 end Lean

src/Lean/AuxRecursor.lean

@@ -56,11 +56,11 @@ def markSparseCasesOn (env : Environment) (declName : Name) : Environment :=
   sparseCasesOnExt.tag env declName
 
 /-- Is this a constructor elimination or a sparse casesOn? -/
-def isSparseCasesOn (env : Environment) (declName : Name) : Bool :=
+public def isSparseCasesOn (env : Environment) (declName : Name) : Bool :=
   sparseCasesOnExt.isTagged env declName
 
 /-- Is this a `.casesOn`, a constructor elimination or a sparse casesOn? -/
-def isCasesOnLike (env : Environment) (declName : Name) : Bool :=
+public def isCasesOnLike (env : Environment) (declName : Name) : Bool :=
   isCasesOnRecursor env declName || isSparseCasesOn env declName
 
 /--

src/Lean/Compiler/InitAttr.lean

@@ -54,7 +54,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
     descr := "initialization procedure for global references"
     -- We want to run `[init]` in declaration order
     preserveOrder := true
-    getParam := fun declName stx => withoutExporting do
+    getParam := fun declName stx => do
       let decl ← getConstInfo declName
       match (← Attribute.Builtin.getIdent? stx) with
       | some initFnName =>
@@ -149,6 +149,8 @@ def setBuiltinInitAttr (env : Environment) (declName : Name) (initFnName : Name
 def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit :=
   -- can always be private, not referenced directly except through emitted C code
   withoutExporting do
+  -- TODO: needs an update-stage0 + prefer_native=true for breaking symbol name
+  withExporting do
     let name ← mkAuxDeclName (kind := `_regBuiltin ++ forDecl)
     let type := mkApp (mkConst `IO) (mkConst `Unit)
     let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,

src/Lean/Compiler/LCNF/EmitC.lean

@@ -774,7 +774,7 @@ where
 
 mutual
 
-partial def emitBasicBlock (code : Code .impure) : EmitM Unit := do
+private partial def emitBasicBlock (code : Code .impure) : EmitM Unit := do
   match code with
   | .jp (k := k) .. => emitBasicBlock k
   | .let decl k =>
@@ -896,7 +896,7 @@ where
   emitUnreach : EmitM Unit := do
     emitLn "lean_internal_panic_unreachable();"
 
-partial def emitJoinPoints (code : Code .impure) : EmitM Unit := do
+private partial def emitJoinPoints (code : Code .impure) : EmitM Unit := do
   match code with
   | .jp decl k =>
     emit decl.binderName; emitLn ":"
@@ -906,7 +906,7 @@ partial def emitJoinPoints (code : Code .impure) : EmitM Unit := do
   | .sset (k := k) .. | .uset (k := k) .. | .oset (k := k) .. => emitJoinPoints k
   | .cases .. | .return .. | .jmp .. | .unreach .. => return ()
 
-partial def emitCode (code : Code .impure) : EmitM Unit := do
+private partial def emitCode (code : Code .impure) : EmitM Unit := do
   withEmitBlock do
     let declared ← declareVars code
     if declared then emitLn ""

src/Lean/Compiler/LCNF/EmitUtil.lean

@@ -12,7 +12,7 @@ import Lean.Compiler.InitAttr
 
 namespace Lean.Compiler.LCNF
 
-structure CollectUsedDeclsState where
+private structure CollectUsedDeclsState where
   visited : NameSet := {}
   localDecls : Array (Decl .impure) := #[]
   extSigs : Array (Signature .impure) := #[]

src/Lean/Compiler/LCNF/PublicDeclsExt.lean

@@ -29,7 +29,7 @@ public def mkOrderedDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
 /--
 Set of declarations to be exported to other modules; visibility shared by base/mono/IR phases.
 -/
-builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
+private builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 
 public def isDeclPublic (env : Environment) (declName : Name) : Bool := Id.run do
   if !env.header.isModule then

src/Lean/Compiler/LCNF/ToExpr.lean

@@ -142,10 +142,10 @@ partial def Code.toExprM (code : Code pu) : ToExprM Expr := do
     return .letE `dummy (mkConst ``Unit) value body true
 end
 
-def Code.toExpr (code : Code pu) (xs : Array FVarId := #[]) : Expr :=
+public def Code.toExpr (code : Code pu) (xs : Array FVarId := #[]) : Expr :=
   run' code.toExprM xs
 
-def FunDecl.toExpr (decl : FunDecl pu) (xs : Array FVarId := #[]) : Expr :=
+public def FunDecl.toExpr (decl : FunDecl pu) (xs : Array FVarId := #[]) : Expr :=
   run' decl.toExprM xs
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -213,22 +213,11 @@ structure Context where
   -/
   expectedType : Option Expr
 
-/--
-Key for the LCNF translation cache. `ignoreNoncomputable` is part of the key
-because entries cached in irrelevant positions skip the `checkComputable`
-check and must not be reused in relevant positions.
--/
-structure CacheKey where
-  expr : Expr
-  expectedType? : Option Expr
-  ignoreNoncomputable : Bool
-  deriving BEq, Hashable
-
 structure State where
   /-- Local context containing the original Lean types (not LCNF ones). -/
   lctx : LocalContext := {}
   /-- Cache from Lean regular expression to LCNF argument. -/
-  cache : PHashMap CacheKey (Arg .pure) := {}
+  cache : PHashMap (Expr × Option Expr) (Arg .pure) := {}
   /--
   Determines whether caching has been disabled due to finding a use of
   a constant marked with `never_extract`.
@@ -484,9 +473,7 @@ partial def toLCNF (e : Expr) (eType : Expr) : CompilerM (Code .pure) := do
 where
   visitCore (e : Expr) : M (Arg .pure) := withIncRecDepth do
     let eType? := (← read).expectedType
-    let ignoreNoncomputable := (← read).ignoreNoncomputable
-    let key : CacheKey := { expr := e, expectedType? := eType?, ignoreNoncomputable }
-    if let some arg := (← get).cache.find? key then
+    if let some arg := (← get).cache.find? (e, eType?) then
       return arg
     let r : Arg .pure ← match e with
       | .app ..      => visitApp e
@@ -498,7 +485,7 @@ where
       | .lit lit     => visitLit lit
       | .fvar fvarId => if (← get).toAny.contains fvarId then pure .erased else pure (.fvar fvarId)
       | .forallE .. | .mvar .. | .bvar .. | .sort ..  => unreachable!
-    modify fun s => if s.shouldCache then { s with cache := s.cache.insert key r } else s
+    modify fun s => if s.shouldCache then { s with cache := s.cache.insert (e, eType?) r } else s
     return r
 
   visit (e : Expr) : M (Arg .pure) := withIncRecDepth do

src/Lean/Compiler/ModPkgExt.lean

@@ -37,7 +37,7 @@ public def getStateByIdx? [Inhabited σ] (ext : ModuleEnvExtension σ) (env : En
 
 end ModuleEnvExtension
 
-initialize modPkgExt : ModuleEnvExtension (Option PkgId) ←
+private initialize modPkgExt : ModuleEnvExtension (Option PkgId) ←
   registerModuleEnvExtension (pure none)
 
 /-- Returns the package (if any) of an imported module (by its index). -/

src/Lean/Compiler/NameDemangling.lean

@@ -20,13 +20,13 @@ line parsing. Called from the C runtime via `@[export]` for backtrace display. -
 namespace Lean.Name.Demangle
 
 /-- `String.dropPrefix?` returning a `String` instead of a `Slice`. -/
-def dropPrefix? (s : String) (pre : String) : Option String :=
+private def dropPrefix? (s : String) (pre : String) : Option String :=
   (s.dropPrefix? pre).map (·.toString)
 
-def isAllDigits (s : String) : Bool :=
+private def isAllDigits (s : String) : Bool :=
   !s.isEmpty && s.all (·.isDigit)
 
-def nameToNameParts (n : Name) : Array NamePart :=
+private def nameToNameParts (n : Name) : Array NamePart :=
   go n [] |>.toArray
 where
   go : Name → List NamePart → List NamePart
@@ -34,17 +34,17 @@ where
     | .str pre s, acc => go pre (NamePart.str s :: acc)
     | .num pre n, acc => go pre (NamePart.num n :: acc)
 
-def namePartsToName (parts : Array NamePart) : Name :=
+private def namePartsToName (parts : Array NamePart) : Name :=
   parts.foldl (fun acc p =>
     match p with
     | .str s => acc.mkStr s
     | .num n => acc.mkNum n) .anonymous
 
 /-- Format name parts using `Name.toString` for correct escaping. -/
-def formatNameParts (comps : Array NamePart) : String :=
+private def formatNameParts (comps : Array NamePart) : String :=
   if comps.isEmpty then "" else (namePartsToName comps).toString
 
-def matchSuffix (c : NamePart) : Option String :=
+private def matchSuffix (c : NamePart) : Option String :=
   match c with
   | NamePart.str s =>
     if s == "_redArg" then some "arity↓"
@@ -58,12 +58,12 @@ def matchSuffix (c : NamePart) : Option String :=
     else none
   | _ => none
 
-def isSpecIndex (c : NamePart) : Bool :=
+private def isSpecIndex (c : NamePart) : Bool :=
   match c with
   | NamePart.str s => (dropPrefix? s "spec_").any isAllDigits
   | _ => false
 
-def stripPrivate (comps : Array NamePart) (start stop : Nat) :
+private def stripPrivate (comps : Array NamePart) (start stop : Nat) :
     Nat × Bool :=
   if stop - start >= 3 && comps[start]? == some (NamePart.str "_private") then
     Id.run do
@@ -75,11 +75,11 @@ def stripPrivate (comps : Array NamePart) (start stop : Nat) :
   else
     (start, false)
 
-structure SpecEntry where
+private structure SpecEntry where
   name : String
   flags : Array String
 
-def processSpecContext (comps : Array NamePart) : SpecEntry := Id.run do
+private def processSpecContext (comps : Array NamePart) : SpecEntry := Id.run do
   let mut begin_ := 0
   if comps.size >= 3 && comps[0]? == some (NamePart.str "_private") then
     for i in [1:comps.size] do
@@ -99,7 +99,7 @@ def processSpecContext (comps : Array NamePart) : SpecEntry := Id.run do
       else parts := parts.push c
   { name := formatNameParts parts, flags }
 
-def postprocessNameParts (components : Array NamePart) : String := Id.run do
+private def postprocessNameParts (components : Array NamePart) : String := Id.run do
   if components.isEmpty then return ""
 
   let (privStart, isPrivate) := stripPrivate components 0 components.size
@@ -206,14 +206,14 @@ def postprocessNameParts (components : Array NamePart) : String := Id.run do
 
   return result
 
-def demangleBody (body : String) : String :=
+private def demangleBody (body : String) : String :=
   let name := Name.demangle body
   postprocessNameParts (nameToNameParts name)
 
 /-- Split a `lp_`-prefixed symbol into (demangled body, package name).
 Tries each underscore as a split point; the first valid split (shortest single-component
 package where the remainder is a valid mangled name) is correct. -/
-def demangleWithPkg (s : String) : Option (String × String) := do
+private def demangleWithPkg (s : String) : Option (String × String) := do
   for ⟨pos, h⟩ in s.positions do
     if pos.get h == '_' && pos ≠ s.startPos then
       let nextPos := pos.next h
@@ -230,12 +230,12 @@ def demangleWithPkg (s : String) : Option (String × String) := do
         return (demangleBody body, pkgName)
   none
 
-def stripColdSuffix (s : String) : String × String :=
+private def stripColdSuffix (s : String) : String × String :=
   match s.find? ".cold" with
   | some pos => (s.extract s.startPos pos, s.extract pos s.endPos)
   | none => (s, "")
 
-def demangleCore (s : String) : Option String := do
+private def demangleCore (s : String) : Option String := do
   -- _init_l_
   if let some body := dropPrefix? s "_init_l_" then
     if !body.isEmpty then return s!"[init] {demangleBody body}"
@@ -291,17 +291,17 @@ public def demangleSymbol (symbol : String) : Option String := do
   if coldSuffix.isEmpty then return result
   else return s!"{result} {coldSuffix}"
 
-def skipWhile (s : String) (pos : s.Pos) (pred : Char → Bool) : s.Pos :=
+private def skipWhile (s : String) (pos : s.Pos) (pred : Char → Bool) : s.Pos :=
   if h : pos = s.endPos then pos
   else if pred (pos.get h) then skipWhile s (pos.next h) pred
   else pos
 termination_by pos
 
-def splitAt₂ (s : String) (p₁ p₂ : s.Pos) : String × String × String :=
+private def splitAt₂ (s : String) (p₁ p₂ : s.Pos) : String × String × String :=
   (s.extract s.startPos p₁, s.extract p₁ p₂, s.extract p₂ s.endPos)
 
 /-- Extract the symbol from a backtrace line (Linux glibc or macOS format). -/
-def extractSymbol (line : String) :
+private def extractSymbol (line : String) :
     Option (String × String × String) :=
   tryLinux line |>.orElse (fun _ => tryMacOS line)
 where

src/Lean/Data/JsonRpc.lean

@@ -400,7 +400,7 @@ Namely:
 def parseMessageMetaData (input : String) : Except String MessageMetaData :=
   messageMetaDataParser input |>.run input
 
-inductive MessageDirection where
+public inductive MessageDirection where
   | clientToServer
   | serverToClient
   deriving Inhabited, FromJson, ToJson

src/Lean/Data/PersistentArray.lean

@@ -227,7 +227,7 @@ variable {β : Type v}
 set_option linter.unusedVariables.funArgs false in
 @[specialize]
 partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [inh : Inhabited β]
-    (f : α → β → m (ForInStep β)) (n : @&PersistentArrayNode α) (b : β) : m (ForInStep β) := do
+    (f : α → β → m (ForInStep β)) (n : PersistentArrayNode α) (b : β) : m (ForInStep β) := do
   let mut b := b
   match n with
   | leaf vs =>
@@ -243,7 +243,7 @@ partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       | ForInStep.yield bNew => b := bNew
     return ForInStep.yield b
 
-@[specialize] protected def forIn (t : @&PersistentArray α) (init : β) (f : α → β → m (ForInStep β)) : m β := do
+@[specialize] protected def forIn (t : PersistentArray α) (init : β) (f : α → β → m (ForInStep β)) : m β := do
   match (← forInAux (inh := ⟨init⟩) f t.root init) with
   | ForInStep.done b  => pure b
   | ForInStep.yield b =>

src/Lean/Data/PersistentHashMap.lean

@@ -153,7 +153,7 @@ partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.s
     else findAtAux keys vals heq (i+1) k
   else none
 
-partial def findAux [BEq α] : @&Node α β → USize → α → Option β
+partial def findAux [BEq α] : Node α β → USize → α → Option β
   | Node.entries entries, h, k =>
     let j     := (mod2Shift h shift).toNat
     match entries[j]! with
@@ -162,7 +162,7 @@ partial def findAux [BEq α] : @&Node α β → USize → α → Option β
     | Entry.entry k' v => if k == k' then some v else none
   | Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
 
-def find? {_ : BEq α} {_ : Hashable α} : @&PersistentHashMap α β → α → Option β
+def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option β
   | { root }, k => findAux root (hash k |>.toUSize) k
 
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
@@ -184,7 +184,7 @@ partial def findEntryAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : k
     else findEntryAtAux keys vals heq (i+1) k
   else none
 
-partial def findEntryAux [BEq α] : @&Node α β → USize → α → Option (α × β)
+partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α × β)
   | Node.entries entries, h, k =>
     let j     := (mod2Shift h shift).toNat
     match entries[j]! with
@@ -193,7 +193,7 @@ partial def findEntryAux [BEq α] : @&Node α β → USize → α → Option (α
     | Entry.entry k' v => if k == k' then some (k', v) else none
   | Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
 
-def findEntry? {_ : BEq α} {_ : Hashable α} : @&PersistentHashMap α β → α → Option (α × β)
+def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option (α × β)
   | { root }, k => findEntryAux root (hash k |>.toUSize) k
 
 partial def findKeyDAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) (k₀ : α) : α :=
@@ -320,7 +320,7 @@ def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ
   Id.run <| map.foldlM (pure <| f · · ·) init
 
 protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
-    (map : @&PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do
+    (map : PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do
   let intoError : ForInStep σ → Except σ σ
   | .done s => .error s
   | .yield s => .ok s

src/Lean/Data/Trie.lean

@@ -131,9 +131,9 @@ partial def find? (t : Trie α) (s : String) : Option α :=
   loop 0 t
 
 /-- Returns an `Array` of all values in the trie, in no particular order. -/
-partial def values (t : @&Trie α) : Array α := go t |>.run #[] |>.2
+partial def values (t : Trie α) : Array α := go t |>.run #[] |>.2
   where
-    go : @&Trie α → StateM (Array α) Unit
+    go : Trie α → StateM (Array α) Unit
       | leaf a? => do
         if let some a := a? then
           modify (·.push a)

src/Lean/DocString/Markdown.lean

@@ -43,14 +43,14 @@ public structure State where
   /-- Footnotes -/
   footnotes : Array (String × String) := #[]
 
-def combineBlocks (prior current : String) :=
+private def combineBlocks (prior current : String) :=
   if prior.isEmpty then current
   else if current.isEmpty then prior
   else if prior.endsWith "\n\n" then prior ++ current
   else if prior.endsWith "\n" then prior ++ "\n" ++ current
   else prior ++ "\n\n" ++ current
 
-def State.endBlock (state : State) : State :=
+private def State.endBlock (state : State) : State :=
   { state with
     priorBlocks :=
       combineBlocks state.priorBlocks state.currentBlock ++
@@ -60,13 +60,13 @@ def State.endBlock (state : State) : State :=
     footnotes := #[]
   }
 
-def State.render (state : State) : String :=
+private def State.render (state : State) : String :=
   state.endBlock.priorBlocks
 
-def State.push (state : State) (txt : String) : State :=
+private def State.push (state : State) (txt : String) : State :=
   { state with currentBlock := state.currentBlock ++ txt }
 
-def State.endsWith (state : State) (txt : String) : Bool :=
+private def State.endsWith (state : State) (txt : String) : Bool :=
   state.currentBlock.endsWith txt || (state.currentBlock.isEmpty && state.priorBlocks.endsWith txt)
 
 end MarkdownM
@@ -150,7 +150,7 @@ public class MarkdownBlock (i : Type u) (b : Type v) where
 public instance : MarkdownBlock i Empty where
   toMarkdown := nofun
 
-def escape (s : String) : String := Id.run do
+private def escape (s : String) : String := Id.run do
   let mut s' := ""
   let mut iter := s.startPos
   while h : ¬iter.IsAtEnd do
@@ -163,7 +163,7 @@ def escape (s : String) : String := Id.run do
 where
   isSpecial c := "*_`-+.!<>[]{}()#".any (· == c)
 
-def quoteCode (str : String) : String := Id.run do
+private def quoteCode (str : String) : String := Id.run do
   let mut longest := 0
   let mut current := 0
   let mut iter := str.startPos
@@ -179,7 +179,7 @@ def quoteCode (str : String) : String := Id.run do
   let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
   backticks ++ str ++ backticks
 
-partial def trimLeft (inline : Inline i) : (String × Inline i) := go [inline]
+private partial def trimLeft (inline : Inline i) : (String × Inline i) := go [inline]
 where
   go : List (Inline i) → String × Inline i
     | [] => ("", .empty)
@@ -194,7 +194,7 @@ where
     | .concat xs :: more => go (xs.toList ++ more)
     | here :: more => ("", here ++ .concat more.toArray)
 
-partial def trimRight (inline : Inline i) : (Inline i × String) := go [inline]
+private partial def trimRight (inline : Inline i) : (Inline i × String) := go [inline]
 where
   go : List (Inline i) → Inline i × String
     | [] => (.empty, "")
@@ -209,13 +209,13 @@ where
     | .concat xs :: more => go (xs.reverse.toList ++ more)
     | here :: more => (.concat more.toArray.reverse ++ here, "")
 
-def trim (inline : Inline i) : (String × Inline i × String) :=
+private def trim (inline : Inline i) : (String × Inline i × String) :=
   let (pre, more) := trimLeft inline
   let (mid, post) := trimRight more
   (pre, mid, post)
 
 open MarkdownM in
-partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM Unit
+private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM Unit
   | .text s =>
     push (escape s)
   | .linebreak s => do
@@ -271,7 +271,7 @@ partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM Unit
 public instance [MarkdownInline i] : ToMarkdown (Inline i) where
   toMarkdown inline := private inlineMarkdown inline
 
-def quoteCodeBlock (indent : Nat) (str : String) : String := Id.run do
+private def quoteCodeBlock (indent : Nat) (str : String) : String := Id.run do
   let mut longest := 2
   let mut current := 0
   let mut iter := str.startPos
@@ -292,7 +292,7 @@ def quoteCodeBlock (indent : Nat) (str : String) : String := Id.run do
   backticks ++ "\n" ++ out ++ backticks ++ "\n"
 
 open MarkdownM in
-partial def blockMarkdown [MarkdownInline i] [MarkdownBlock i b] : Block i b → MarkdownM Unit
+private partial def blockMarkdown [MarkdownInline i] [MarkdownBlock i b] : Block i b → MarkdownM Unit
   | .para xs => do
     for i in xs do
       ToMarkdown.toMarkdown i
@@ -345,7 +345,7 @@ public instance [MarkdownInline i] [MarkdownBlock i b] : ToMarkdown (Block i b)
 
 open MarkdownM in
 open ToMarkdown in
-partial def partMarkdown [MarkdownInline i] [MarkdownBlock i b] (level : Nat) (part : Part i b p) : MarkdownM Unit := do
+private partial def partMarkdown [MarkdownInline i] [MarkdownBlock i b] (level : Nat) (part : Part i b p) : MarkdownM Unit := do
   push ("".pushn '#' (level + 1))
   push " "
   for i in part.title do

src/Lean/DocString/Parser.lean

@@ -18,7 +18,7 @@ open Lean.Doc.Syntax
 local instance : Coe Char ParserFn where
   coe := chFn
 
-partial def atLeastAux (n : Nat) (p : ParserFn) : ParserFn := fun c s => Id.run do
+private partial def atLeastAux (n : Nat) (p : ParserFn) : ParserFn := fun c s => Id.run do
   let iniSz  := s.stackSize
   let iniPos := s.pos
   let mut s  := p c s
@@ -30,7 +30,7 @@ partial def atLeastAux (n : Nat) (p : ParserFn) : ParserFn := fun c s => Id.run
     s := s.mkNode nullKind iniSz
   atLeastAux (n - 1) p c s
 
-def atLeastFn (n : Nat) (p : ParserFn) : ParserFn := fun c s =>
+private def atLeastFn (n : Nat) (p : ParserFn) : ParserFn := fun c s =>
   let iniSz  := s.stackSize
   let s := atLeastAux n p c s
   s.mkNode nullKind iniSz
@@ -40,9 +40,9 @@ A parser that does nothing.
 -/
 public def skipFn : ParserFn := fun _ s => s
 
-def eatSpaces := takeWhileFn (· == ' ')
+private def eatSpaces := takeWhileFn (· == ' ')
 
-def repFn : Nat → ParserFn → ParserFn
+private def repFn : Nat → ParserFn → ParserFn
   | 0, _ => skipFn
   | n+1, p => p >> repFn n p
 
@@ -55,7 +55,7 @@ partial def satisfyFn' (p : Char → Bool)
   else if p (c.get' i h) then s.next' c i h
   else s.mkUnexpectedError errorMsg
 
-partial def atMostAux (n : Nat) (p : ParserFn) (msg : String) : ParserFn :=
+private partial def atMostAux (n : Nat) (p : ParserFn) (msg : String) : ParserFn :=
   fun c s => Id.run do
     let iniSz  := s.stackSize
     let iniPos := s.pos
@@ -70,13 +70,13 @@ partial def atMostAux (n : Nat) (p : ParserFn) (msg : String) : ParserFn :=
       s := s.mkNode nullKind iniSz
     atMostAux (n - 1) p msg c s
 
-def atMostFn (n : Nat) (p : ParserFn) (msg : String) : ParserFn := fun c s =>
+private def atMostFn (n : Nat) (p : ParserFn) (msg : String) : ParserFn := fun c s =>
   let iniSz  := s.stackSize
   let s := atMostAux n p msg c s
   s.mkNode nullKind iniSz
 
 /-- Like `satisfyFn`, but allows any escape sequence through -/
-partial def satisfyEscFn (p : Char → Bool)
+private partial def satisfyEscFn (p : Char → Bool)
     (errorMsg : String := "unexpected character") :
     ParserFn := fun c s =>
   let i := s.pos
@@ -89,7 +89,7 @@ partial def satisfyEscFn (p : Char → Bool)
   else if p (c.get' i h) then s.next' c i h
   else s.mkUnexpectedError errorMsg
 
-partial def takeUntilEscFn (p : Char → Bool) : ParserFn := fun c s =>
+private partial def takeUntilEscFn (p : Char → Bool) : ParserFn := fun c s =>
   let i := s.pos
   if h : c.atEnd i then s
   else if c.get' i h == '\\' then
@@ -100,7 +100,7 @@ partial def takeUntilEscFn (p : Char → Bool) : ParserFn := fun c s =>
   else if p (c.get' i h) then s
   else takeUntilEscFn p c (s.next' c i h)
 
-partial def takeWhileEscFn (p : Char → Bool) : ParserFn := takeUntilEscFn (not ∘ p)
+private partial def takeWhileEscFn (p : Char → Bool) : ParserFn := takeUntilEscFn (not ∘ p)
 
 /--
 Parses as `p`, but discards the result.
@@ -111,7 +111,7 @@ public def ignoreFn (p : ParserFn) : ParserFn := fun c s =>
   s'.shrinkStack iniSz
 
 
-def withInfoSyntaxFn (p : ParserFn) (infoP : SourceInfo → ParserFn) : ParserFn := fun c s =>
+private def withInfoSyntaxFn (p : ParserFn) (infoP : SourceInfo → ParserFn) : ParserFn := fun c s =>
   let iniSz := s.stxStack.size
   let startPos := s.pos
   let s := p c s
@@ -121,7 +121,7 @@ def withInfoSyntaxFn (p : ParserFn) (infoP : SourceInfo → ParserFn) : ParserFn
   let info     := SourceInfo.original leading startPos trailing stopPos
   infoP info c (s.shrinkStack iniSz)
 
-def unescapeStr (str : String) : String := Id.run do
+private def unescapeStr (str : String) : String := Id.run do
   let mut out := ""
   let mut iter := str.startPos
   while h : ¬iter.IsAtEnd do
@@ -135,7 +135,7 @@ def unescapeStr (str : String) : String := Id.run do
       out := out.push c
   out
 
-def asStringAux (quoted : Bool) (startPos : String.Pos.Raw) (transform : String → String) :
+private def asStringAux (quoted : Bool) (startPos : String.Pos.Raw) (transform : String → String) :
     ParserFn := fun c s =>
   let stopPos  := s.pos
   let leading  := c.mkEmptySubstringAt startPos
@@ -156,26 +156,26 @@ public def asStringFn (p : ParserFn) (quoted := false) (transform : String → S
   if s.hasError then s
   else asStringAux quoted startPos transform c (s.shrinkStack iniSz)
 
-def checkCol0Fn (errorMsg : String) : ParserFn := fun c s =>
+private def checkCol0Fn (errorMsg : String) : ParserFn := fun c s =>
   let pos      := c.fileMap.toPosition s.pos
   if pos.column = 1 then s
   else s.mkError errorMsg
 
-def _root_.Lean.Parser.ParserContext.currentColumn
+private def _root_.Lean.Parser.ParserContext.currentColumn
     (c : ParserContext) (s : ParserState) : Nat :=
   c.fileMap.toPosition s.pos |>.column
 
-def pushColumn : ParserFn := fun c s =>
+private def pushColumn : ParserFn := fun c s =>
   let col := c.fileMap.toPosition s.pos |>.column
   s.pushSyntax <| Syntax.mkLit `column (toString col) (SourceInfo.synthetic s.pos s.pos)
 
-def guardColumn (p : Nat → Bool) (message : String) : ParserFn := fun c s =>
+private def guardColumn (p : Nat → Bool) (message : String) : ParserFn := fun c s =>
   if p (c.currentColumn s) then s else s.mkErrorAt message s.pos
 
-def guardMinColumn (min : Nat) (description : String := s!"expected column at least {min}") : ParserFn :=
+private def guardMinColumn (min : Nat) (description : String := s!"expected column at least {min}") : ParserFn :=
   guardColumn (· ≥ min) description
 
-def withCurrentColumn (p : Nat → ParserFn) : ParserFn := fun c s =>
+private def withCurrentColumn (p : Nat → ParserFn) : ParserFn := fun c s =>
   p (c.currentColumn s) c s
 
 
@@ -183,7 +183,7 @@ def withCurrentColumn (p : Nat → ParserFn) : ParserFn := fun c s =>
 We can only start a nestable block if we're immediately after a newline followed by a sequence of
 nestable block openers
 -/
-def onlyBlockOpeners : ParserFn := fun c s =>
+private def onlyBlockOpeners : ParserFn := fun c s =>
   let position := c.fileMap.toPosition s.pos
   let lineStart := c.fileMap.lineStart position.line
   let ok : Bool := Id.run do
@@ -206,7 +206,7 @@ def onlyBlockOpeners : ParserFn := fun c s =>
   if ok then s
   else s.mkErrorAt "beginning of line or sequence of nestable block openers" s.pos
 
-def nl := satisfyFn (· == '\n') "newline"
+private def nl := satisfyFn (· == '\n') "newline"
 
 /--
 Construct a “fake” atom with the given string content and source information.
@@ -225,13 +225,13 @@ current position.
 Normally, atoms are always substrings of the original input; however, Verso's concrete syntax is
 different enough from Lean's that this isn't always a good match.
 -/
-def fakeAtomHere (str : String) : ParserFn :=
+private def fakeAtomHere (str : String) : ParserFn :=
   withInfoSyntaxFn skip.fn (fun info => fakeAtom str (info := info))
 
-def pushMissing : ParserFn := fun _c s =>
+private def pushMissing : ParserFn := fun _c s =>
   s.pushSyntax .missing
 
-def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
+private def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
   let rec go (iter : str.Pos) (s : ParserState) :=
     if h : iter.IsAtEnd then s
     else
@@ -260,10 +260,10 @@ public instance : Ord OrderedListType where
     | .parenAfter, .numDot => .gt
     | .parenAfter, .parenAfter => .eq
 
-def OrderedListType.all : List OrderedListType :=
+private def OrderedListType.all : List OrderedListType :=
   [.numDot, .parenAfter]
 
-theorem OrderedListType.all_complete : ∀ x : OrderedListType, x ∈ all := by
+private theorem OrderedListType.all_complete : ∀ x : OrderedListType, x ∈ all := by
   unfold all; intro x; cases x <;> repeat constructor
 
 /--
@@ -288,40 +288,40 @@ public instance : Ord UnorderedListType where
     | .plus, .plus => .eq
     | .plus, _ => .gt
 
-def UnorderedListType.all : List UnorderedListType :=
+private def UnorderedListType.all : List UnorderedListType :=
   [.asterisk, .dash, .plus]
 
-theorem UnorderedListType.all_complete : ∀ x : UnorderedListType, x ∈ all := by
+private theorem UnorderedListType.all_complete : ∀ x : UnorderedListType, x ∈ all := by
   unfold all; intro x; cases x <;> repeat constructor
 
-def unorderedListIndicator (type : UnorderedListType) : ParserFn :=
+private def unorderedListIndicator (type : UnorderedListType) : ParserFn :=
   asStringFn <|
     match type with
     | .asterisk => chFn '*'
     | .dash => chFn '-'
     | .plus => chFn '+'
 
-def orderedListIndicator (type : OrderedListType) : ParserFn :=
+private def orderedListIndicator (type : OrderedListType) : ParserFn :=
   asStringFn <|
     takeWhile1Fn (·.isDigit) "digits" >>
     match type with
     | .numDot => chFn '.'
     | .parenAfter => chFn ')'
 
-def blankLine : ParserFn :=
+private def blankLine : ParserFn :=
   nodeFn `blankLine <| atomicFn <| asStringFn <| takeWhileFn (· == ' ') >> nl
 
-def endLine : ParserFn :=
+private def endLine : ParserFn :=
   ignoreFn <| atomicFn <| asStringFn <| takeWhileFn (· == ' ') >> eoiFn
 
-def bullet := atomicFn (go UnorderedListType.all)
+private def bullet := atomicFn (go UnorderedListType.all)
 where
   go
     | [] => fun _ s => s.mkError "no list type"
     | [x] => atomicFn (unorderedListIndicator x)
     | x :: xs => atomicFn (unorderedListIndicator x) <|> go xs
 
-def numbering := atomicFn (go OrderedListType.all)
+private def numbering := atomicFn (go OrderedListType.all)
 where
   go
     | [] => fun _ s => s.mkError "no list type"
@@ -374,7 +374,7 @@ public def inlineTextChar : ParserFn := fun c s =>
 /-- Return some inline text up to the next inline opener or the end of
 the line, whichever is first. Always consumes at least one
 logical character on success, taking escaping into account. -/
-def inlineText : ParserFn :=
+private def inlineText : ParserFn :=
   asStringFn (transform := unescapeStr) <| atomicFn inlineTextChar >> manyFn inlineTextChar
 
 /--
@@ -410,23 +410,23 @@ public def val : ParserFn := fun c s =>
     else
       s.mkError "expected identifier, string, or number"
 
-def withCurrentStackSize (p : Nat → ParserFn) : ParserFn := fun c s =>
+private def withCurrentStackSize (p : Nat → ParserFn) : ParserFn := fun c s =>
   p s.stxStack.size c s
 
 /-- Match the character indicated, pushing nothing to the stack in case of success -/
-def skipChFn (c : Char) : ParserFn :=
+private def skipChFn (c : Char) : ParserFn :=
   satisfyFn (· == c) c.toString
 
-def skipToNewline : ParserFn :=
+private def skipToNewline : ParserFn :=
     takeUntilFn (· == '\n')
 
-def skipToSpace : ParserFn :=
+private def skipToSpace : ParserFn :=
     takeUntilFn (· == ' ')
 
-def skipRestOfLine : ParserFn :=
+private def skipRestOfLine : ParserFn :=
     skipToNewline >> (eoiFn <|> nl)
 
-def skipBlock : ParserFn :=
+private def skipBlock : ParserFn :=
   skipToNewline >> manyFn nonEmptyLine >> takeWhileFn (· == '\n')
 where
   nonEmptyLine : ParserFn :=
@@ -444,7 +444,7 @@ public def recoverBlock (p : ParserFn) (final : ParserFn := skipFn) : ParserFn :
     ignoreFn skipBlock >> final
 
 -- Like `recoverBlock` but stores recovered errors at the original error position.
-def recoverBlockAtErrPos (p : ParserFn) : ParserFn := fun c s =>
+private def recoverBlockAtErrPos (p : ParserFn) : ParserFn := fun c s =>
   let s := p c s
   if let some msg := s.errorMsg then
     let errPos := s.pos
@@ -457,36 +457,36 @@ def recoverBlockAtErrPos (p : ParserFn) : ParserFn := fun c s =>
       recoveredErrors := s.recoveredErrors.push (errPos, s'.stxStack, msg)}
   else s
 
-def recoverBlockWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
+private def recoverBlockWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     ignoreFn skipBlock >>
     show ParserFn from
       fun _ s => stxs.foldl (init := s.shrinkStack rctx.initialSize) (·.pushSyntax ·)
 
-def recoverLine (p : ParserFn) : ParserFn :=
+private def recoverLine (p : ParserFn) : ParserFn :=
   recoverFn p fun _ =>
     ignoreFn skipRestOfLine
 
-def recoverWs (p : ParserFn) : ParserFn :=
+private def recoverWs (p : ParserFn) : ParserFn :=
   recoverFn p fun _ =>
     ignoreFn <| takeUntilFn (fun c =>  c == ' ' || c == '\n')
 
-def recoverNonSpace (p : ParserFn) : ParserFn :=
+private def recoverNonSpace (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     ignoreFn (takeUntilFn (fun c => c != ' ')) >>
     show ParserFn from
       fun _ s => s.shrinkStack rctx.initialSize
 
-def recoverWsWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
+private def recoverWsWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     ignoreFn <| takeUntilFn (fun c =>  c == ' ' || c == '\n') >>
     show ParserFn from
       fun _ s => stxs.foldl (init := s.shrinkStack rctx.initialSize) (·.pushSyntax ·)
 
-def recoverEol (p : ParserFn) : ParserFn :=
+private def recoverEol (p : ParserFn) : ParserFn :=
   recoverFn p fun _ => ignoreFn <| skipToNewline
 
-def recoverEolWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
+private def recoverEolWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     ignoreFn skipToNewline >>
     show ParserFn from
@@ -494,7 +494,7 @@ def recoverEolWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
 
 -- Like `recoverEol` but stores recovered errors at the original error position
 -- rather than the post-recovery position.
-def recoverEolAtErrPos (p : ParserFn) : ParserFn := fun c s =>
+private def recoverEolAtErrPos (p : ParserFn) : ParserFn := fun c s =>
   let s := p c s
   if let some msg := s.errorMsg then
     let errPos := s.pos
@@ -509,7 +509,7 @@ def recoverEolAtErrPos (p : ParserFn) : ParserFn := fun c s =>
 
 -- Like `recoverEolWith` but stores recovered errors at the original error position
 -- rather than the post-recovery position.
-def recoverEolWithAtErrPos (stxs : Array Syntax) (p : ParserFn) : ParserFn := fun c s =>
+private def recoverEolWithAtErrPos (stxs : Array Syntax) (p : ParserFn) : ParserFn := fun c s =>
   let iniSz := s.stxStack.size
   let s := p c s
   if let some msg := s.errorMsg then
@@ -521,10 +521,10 @@ def recoverEolWithAtErrPos (stxs : Array Syntax) (p : ParserFn) : ParserFn := fu
       {s' with recoveredErrors := s.recoveredErrors.push (errPos, s'.stxStack, msg)}
   else s
 
-def recoverSkip (p : ParserFn) : ParserFn :=
+private def recoverSkip (p : ParserFn) : ParserFn :=
   recoverFn p fun _ => skipFn
 
-def recoverSkipWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
+private def recoverSkipWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     show ParserFn from
       fun _ s => stxs.foldl (init := s.shrinkStack rctx.initialSize) (·.pushSyntax ·)
@@ -535,7 +535,7 @@ def recoverHereWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
     show ParserFn from
       fun _ s => stxs.foldl (init := s.restore rctx.initialSize rctx.initialPos) (·.pushSyntax ·)
 
-def recoverHereWithKeeping (stxs : Array Syntax) (keep : Nat) (p : ParserFn) : ParserFn :=
+private def recoverHereWithKeeping (stxs : Array Syntax) (keep : Nat) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     show ParserFn from
       fun _ s => stxs.foldl (init := s.restore (rctx.initialSize + keep) rctx.initialPos) (·.pushSyntax ·)
@@ -584,7 +584,7 @@ it's in a single-line context and whitespace may only be the space
 character. If it's `some N`, then newlines are allowed, but `N` is the
 minimum indentation column.
 -/
-def nameArgWhitespace : (multiline : Option Nat) → ParserFn
+private def nameArgWhitespace : (multiline : Option Nat) → ParserFn
   | none => eatSpaces
   | some n => takeWhileFn (fun c => c == ' ' || c == '\n') >> guardMinColumn n
 
@@ -598,7 +598,7 @@ each sub-parser of `delimitedInline` contributes a clear expected-token name, an
 unhelpful generic "unexpected" messages from inner parsers so that the more informative message
 from `inlineTextChar` survives error merging via `<|>`.
 -/
-def expectedFn (msg : String) (p : ParserFn) : ParserFn := fun c s =>
+private def expectedFn (msg : String) (p : ParserFn) : ParserFn := fun c s =>
   let iniPos := s.pos
   let s := p c s
   if s.hasError && s.pos == iniPos then
@@ -649,18 +649,18 @@ def linebreak (ctxt : InlineCtxt) : ParserFn :=
   else
     errorFn "Newlines not allowed here"
 
-partial def notInLink (ctxt : InlineCtxt) : ParserFn := fun _ s =>
+private partial def notInLink (ctxt : InlineCtxt) : ParserFn := fun _ s =>
   if ctxt.inLink then s.mkError "Already in a link" else s
 
 -- Like `satisfyFn (· == '\n')` but with a better error message that mentions what was expected.
-def newlineOrUnexpected (msg : String) : ParserFn := fun c s =>
+private def newlineOrUnexpected (msg : String) : ParserFn := fun c s =>
   let i := s.pos
   if h : c.atEnd i then s.mkEOIError
   else if c.get' i h == '\n' then s.next' c i h
   else s.mkUnexpectedError s!"unexpected '{c.get' i h}'" [msg]
 
 mutual
-  partial def emphLike
+  private partial def emphLike
     (name : SyntaxNodeKind) (char : Char) (what plural : String)
     (getter : InlineCtxt → Option Nat) (setter : InlineCtxt → Option Nat → InlineCtxt)
     (ctxt : InlineCtxt) : ParserFn :=
@@ -799,7 +799,7 @@ mutual
         nodeFn `str (asStringFn (quoted := true) (many1Fn (satisfyEscFn (fun c => c != ']' && c != '\n') "other than ']' or newline"))) >>
         strFn "]")
 
-  partial def linkTarget : ParserFn := fun c s =>
+  private partial def linkTarget : ParserFn := fun c s =>
     let s := (ref <|> url) c s
     if s.hasError then
       match s.errorMsg with
@@ -922,7 +922,7 @@ deriving Inhabited, Repr
 Finds the minimum column of the first non-whitespace character on each non-empty content line
 between `startPos` and `endPos`, returning `init` if no such line exists.
 -/
-def minContentIndent (text : FileMap) (startPos endPos : String.Pos.Raw)
+private def minContentIndent (text : FileMap) (startPos endPos : String.Pos.Raw)
     (init : Nat) : Nat := Id.run do
   let mut result := init
   let mut thisLineCol := 0
@@ -980,13 +980,13 @@ public def BlockCtxt.forDocString (text : FileMap)
       else text.source.rawEndPos
     { docStartPosition := text.toPosition pos, baseColumn }
 
-def bol (ctxt : BlockCtxt) : ParserFn := fun c s =>
+private def bol (ctxt : BlockCtxt) : ParserFn := fun c s =>
   let pos := c.fileMap.toPosition s.pos
   if pos.column ≤ ctxt.baseColumn then s
   else if pos.line == ctxt.docStartPosition.line && pos.column ≤ ctxt.docStartPosition.column then s
   else s.mkErrorAt s!"beginning of line at {pos}" s.pos
 
-def bolThen (ctxt : BlockCtxt) (p : ParserFn) (description : String) : ParserFn := fun c s =>
+private def bolThen (ctxt : BlockCtxt) (p : ParserFn) (description : String) : ParserFn := fun c s =>
   let position := c.fileMap.toPosition s.pos
   let positionOk :=
     position.column ≤ ctxt.baseColumn ||
@@ -1075,16 +1075,16 @@ public def lookaheadUnorderedListIndicator (ctxt : BlockCtxt) (p : UnorderedList
     if s.hasError then s.setPos iniPos
     else p type c (s.shrinkStack iniSz |>.setPos bulletPos)
 
-def skipUntilDedent (indent : Nat) : ParserFn :=
+private def skipUntilDedent (indent : Nat) : ParserFn :=
   skipRestOfLine >>
   manyFn (chFn ' ' >> takeWhileFn (· == ' ') >> guardColumn (· ≥ indent) s!"indentation at {indent}" >> skipRestOfLine)
 
-def recoverUnindent (indent : Nat) (p : ParserFn) (finish : ParserFn := skipFn) :
+private def recoverUnindent (indent : Nat) (p : ParserFn) (finish : ParserFn := skipFn) :
     ParserFn :=
   recoverFn p (fun _ => ignoreFn (skipUntilDedent indent) >> finish)
 
 
-def blockSep := ignoreFn (manyFn blankLine >> optionalFn endLine)
+private def blockSep := ignoreFn (manyFn blankLine >> optionalFn endLine)
 
 mutual
   /-- Parses a list item according to the current nesting context. -/

src/Lean/Elab/App.lean

@@ -13,7 +13,6 @@ public import Lean.IdentifierSuggestion
 import all Lean.Elab.ErrorUtils
 import Lean.Elab.DeprecatedArg
 import Init.Omega
-import Init.Data.List.MapIdx
 
 public section
 
@@ -1300,13 +1299,13 @@ where
 inductive LValResolution where
   /-- When applied to `f`, effectively expands to `BaseStruct.fieldName (self := Struct.toBase f)`.
   This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied. -/
-  | projFn   (baseStructName : Name) (structName : Name) (fieldName : Name) (levels : List Level)
+  | projFn   (baseStructName : Name) (structName : Name) (fieldName : Name)
   /-- Similar to `projFn`, but for extracting field indexed by `idx`. Works for one-constructor inductive types in general. -/
   | projIdx  (structName : Name) (idx : Nat)
   /-- When applied to `f`, effectively expands to `constName ... (Struct.toBase f)`, with the argument placed in the correct
   positional argument if possible, or otherwise as a named argument. The `Struct.toBase` is not present if `baseStructName == structName`,
   in which case these do not need to be structures. Supports generalized field notation. -/
-  | const    (baseStructName : Name) (structName : Name) (constName : Name) (levels : List Level)
+  | const    (baseStructName : Name) (structName : Name) (constName : Name)
   /-- Like `const`, but with `fvar` instead of `constName`.
   The `baseName` is the base name of the type to search for in the parameter list. -/
   | localRec (baseName : Name) (fvar : Expr)
@@ -1381,7 +1380,7 @@ private def reverseFieldLookup (env : Environment) (fieldName : String) :=
 
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
   match eType.getAppFn, lval with
-  | .const structName _, LVal.fieldIdx ref idx levels =>
+  | .const structName _, LVal.fieldIdx ref idx =>
     if idx == 0 then
       throwError "Invalid projection: Index must be greater than 0"
     let env ← getEnv
@@ -1394,14 +1393,10 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       if idx - 1 < numFields then
         if isStructure env structName then
           let fieldNames := getStructureFields env structName
-          return LValResolution.projFn structName structName fieldNames[idx - 1]! levels
+          return LValResolution.projFn structName structName fieldNames[idx - 1]!
         else
           /- `structName` was declared using `inductive` command.
             So, we don't projection functions for it. Thus, we use `Expr.proj` -/
-          unless levels.isEmpty do
-            throwError "Invalid projection: Explicit universe levels are only supported for inductive types \
-              defined using the `structure` command. \
-              The expression{indentExpr e}\nhas type{inlineExpr eType}which is not a `structure`."
           return LValResolution.projIdx structName (idx - 1)
       else
         if numFields == 0 then
@@ -1414,33 +1409,31 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           ++ MessageData.note m!"The expression{indentExpr e}\nhas type{inlineExpr eType}which has only \
           {numFields} field{numFields.plural}"
           ++ tupleHint
-  | .const structName _, LVal.fieldName ref fieldName levels _ _ => withRef ref do
+  | .const structName _, LVal.fieldName ref fieldName _ _ => withRef ref do
     let env ← getEnv
     if isStructure env structName then
       if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
-        return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName) levels
+        return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName)
     -- Search the local context first
     let fullName := Name.mkStr (privateToUserName structName) fieldName
     for localDecl in (← getLCtx) do
       if localDecl.isAuxDecl then
         if let some localDeclFullName := (← getLCtx).auxDeclToFullName.get? localDecl.fvarId then
           if fullName == privateToUserName localDeclFullName then
-            unless levels.isEmpty do
-              throwInvalidExplicitUniversesForLocal localDecl.toExpr
             /- LVal notation is being used to make a "local" recursive call. -/
             return LValResolution.localRec structName localDecl.toExpr
     -- Then search the environment
     if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then
-      return LValResolution.const baseStructName structName fullName levels
+      return LValResolution.const baseStructName structName fullName
     throwInvalidFieldAt ref fieldName fullName
       -- Suggest a potential unreachable private name as hint. This does not cover structure
       -- inheritance, nor `import all`.
       (declHint := (mkPrivateName env structName).mkStr fieldName)
 
-  | .forallE .., LVal.fieldName ref fieldName levels suffix? fullRef =>
+  | .forallE .., LVal.fieldName ref fieldName suffix? fullRef =>
     let fullName := Name.str `Function fieldName
     if (← getEnv).contains fullName then
-      return LValResolution.const `Function `Function fullName levels
+      return LValResolution.const `Function `Function fullName
     match e.getAppFn, suffix? with
     | Expr.const c _, some suffix =>
       throwUnknownNameWithSuggestions (idOrConst := "constant")  (ref? := fullRef) (c ++ suffix)
@@ -1450,7 +1443,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     throwError "Invalid projection: Projections cannot be used on functions, and{indentExpr e}\n\
       has function type{inlineExprTrailing eType}"
 
-  | .mvar .., .fieldName _ fieldName levels _ _ =>
+  | .mvar .., .fieldName _ fieldName _ _ =>
     let hint := match reverseFieldLookup (← getEnv) fieldName with
       | #[] => MessageData.nil
       | #[opt] => .hint' m!"Consider replacing the field projection `.{fieldName}` with a call to the function `{.ofConstName opt}`."
@@ -1458,13 +1451,13 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           {MessageData.joinSep (opts.toList.map (indentD m!"• `{.ofConstName ·}`")) .nil}"
     throwNamedError lean.invalidField (m!"Invalid field notation: Type of{indentExpr e}\nis not \
       known; cannot resolve field `{fieldName}`" ++ hint)
-  | .mvar .., .fieldIdx _ i _ =>
+  | .mvar .., .fieldIdx _ i  =>
     throwError m!"Invalid projection: Type of{indentExpr e}\nis not known; cannot resolve \
       projection `{i}`"
 
   | _, _ =>
     match e.getAppFn, lval with
-    | Expr.const c _, .fieldName _ref _fieldName _levels (some suffix) fullRef =>
+    | Expr.const c _, .fieldName _ref _fieldName (some suffix) fullRef =>
       throwUnknownNameWithSuggestions (idOrConst := "constant") (ref? := fullRef) (c ++ suffix)
     | _, .fieldName .. =>
       throwNamedError lean.invalidField m!"Invalid field notation: Field projection operates on \
@@ -1713,12 +1706,12 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       let f ← mkProjAndCheck structName idx f
       let f ← addTermInfo lval.getRef f
       loop f lvals
-    | LValResolution.projFn baseStructName structName fieldName levels =>
+    | LValResolution.projFn baseStructName structName fieldName =>
       let f ← mkBaseProjections baseStructName structName f
       let some info := getFieldInfo? (← getEnv) baseStructName fieldName | unreachable!
       if (← isInaccessiblePrivateName info.projFn) then
         throwError "Field `{fieldName}` from structure `{structName}` is private"
-      let projFn ← withRef lval.getRef <| mkConst info.projFn levels
+      let projFn ← withRef lval.getRef <| mkConst info.projFn
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
@@ -1726,9 +1719,9 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       else
         let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
         loop f lvals
-    | LValResolution.const baseStructName structName constName levels =>
+    | LValResolution.const baseStructName structName constName =>
       let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
-      let projFn ← withRef lval.getRef <| mkConst constName levels
+      let projFn ← withRef lval.getRef <| mkConst constName
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let (args, namedArgs) ← addLValArg baseStructName f args namedArgs projFn explicit
@@ -1779,19 +1772,15 @@ false, no elaboration function executed by `x` will reset it to
 /--
 Elaborates the resolutions of a function. The `fns` array is the output of `resolveName'`.
 -/
-private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax × List Level)) (lvals : List LVal)
+private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax)) (lvals : List LVal)
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool)
     (acc : Array (TermElabResult Expr)) (forceTermInfo : Bool := false) :
     TermElabM (Array (TermElabResult Expr)) := do
   let overloaded := overloaded || fns.length > 1
   -- Set `errToSorry` to `false` if `fns` > 1. See comment above about the interaction between `errToSorry` and `observing`.
   withReader (fun ctx => { ctx with errToSorry := fns.length == 1 && ctx.errToSorry }) do
-    fns.foldlM (init := acc) fun acc (f, fIdent, fields, projLevels) => do
-      let lastIdx := fields.length - 1
-      let lvals' := fields.mapIdx fun idx field =>
-        let suffix? := if idx == 0       then some <| toName fields else none
-        let levels  := if idx == lastIdx then projLevels            else []
-        LVal.fieldName field field.getId.getString! levels suffix? fRef
+    fns.foldlM (init := acc) fun acc (f, fIdent, fields) => do
+      let lvals' := toLVals fields (first := true)
       let s ← observing do
         checkDeprecated fIdent f
         let f ← addTermInfo fIdent f expectedType? (force := forceTermInfo)
@@ -1805,6 +1794,11 @@ where
       | field :: fields => .mkStr (go fields) field.getId.toString
     go fields.reverse
 
+  toLVals : List Syntax → (first : Bool) → List LVal
+    | [],            _     => []
+    | field::fields, true  => .fieldName field field.getId.getString! (toName (field::fields)) fRef :: toLVals fields false
+    | field::fields, false => .fieldName field field.getId.getString! none fRef :: toLVals fields false
+
 private def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level) (lvals : List LVal)
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool)
     (acc : Array (TermElabResult Expr)) :
@@ -1838,7 +1832,7 @@ To infer a namespace from the expected type, we do the following operations:
 - if the type is of the form `c x₁ ... xₙ` with `c` a constant, then try using `c` as the namespace,
   and if that doesn't work, try unfolding the expression and continuing.
 -/
-private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax × List Level)) := do
+private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
   unless id.isAtomic do
     throwError "Invalid dotted identifier notation: The name `{id}` must be atomic"
   tryPostponeIfNoneOrMVar expectedType?
@@ -1850,7 +1844,7 @@ private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitU
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
-  throwNoExpectedType {α} : TermElabM α := do
+  throwNoExpectedType := do
     let hint ← match reverseFieldLookup (← getEnv) (id.getString!) with
       | #[] => pure MessageData.nil
       | suggestions =>
@@ -1869,7 +1863,7 @@ where
         withForallBody body k
     else
       k type
-  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax × List Level)) := do
+  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax)) := do
     let resultType ← instantiateMVars resultType
     let resultTypeFn := resultType.getAppFn
     try
@@ -1886,11 +1880,11 @@ where
           |>.filter (fun (_, fieldList) => fieldList.isEmpty)
           |>.map Prod.fst
         if !candidates.isEmpty then
-          candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, [], [])
+          candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, [])
         else if let some (fvar, []) ← resolveLocalName fullName then
           unless explicitUnivs.isEmpty do
             throwInvalidExplicitUniversesForLocal fvar
-          return [(fvar, ← getRef, [], [])]
+          return [(fvar, ← getRef, [])]
         else
           throwUnknownIdentifierAt (← getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`"
             ++ .note m!"Inferred this name from the expected resulting type of `.{id}`:{indentExpr expectedType}"
@@ -1920,37 +1914,26 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     withReader (fun ctx => { ctx with errToSorry := false }) do
       f.getArgs.foldlM (init := acc) fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc
   else
-    let elabFieldName (e field : Syntax) (explicitUnivs : List Level) := do
-      let comps := field.identComponents
-      let lastIdx := comps.length - 1
-      let newLVals := comps.mapIdx fun idx comp =>
-        let levels := if idx = lastIdx then explicitUnivs else []
-        let suffix? := none -- We use `none` since the field can't be part of a composite name
-        LVal.fieldName comp comp.getId.getString! levels suffix? f
+    let elabFieldName (e field : Syntax) (explicit : Bool) := do
+      let newLVals := field.identComponents.map fun comp =>
+        -- We use `none` in `suffix?` since `field` can't be part of a composite name
+        LVal.fieldName comp comp.getId.getString! none f
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    let elabFieldIdx (e idxStx : Syntax) (explicitUnivs : List Level) := do
+    let elabFieldIdx (e idxStx : Syntax) (explicit : Bool) := do
       let some idx := idxStx.isFieldIdx?
         | throwError "Internal error: Unexpected field index syntax `{idxStx}`"
-      elabAppFn e (LVal.fieldIdx idxStx idx explicitUnivs :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) : TermElabM (Array (TermElabResult Expr)) := do
+      elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
+    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) (explicit : Bool) : TermElabM (Array (TermElabResult Expr)) := do
       let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes explicitUnivs expectedType?
       -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
       elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
     match f with
-    | `($(e).$idx:fieldIdx)
-    | `($e |>.$idx:fieldIdx) =>
-      elabFieldIdx e idx []
-    | `($(e).$idx:fieldIdx.{$us,*})
-    | `($e |>.$idx:fieldIdx.{$us,*}) =>
-      let us ← elabExplicitUnivs us
-      elabFieldIdx e idx us
-    | `($(e).$field:ident)
-    | `($e |>.$field:ident) =>
-      elabFieldName e field []
-    | `($(e).$field:ident.{$us,*})
-    | `($e |>.$field:ident.{$us,*}) =>
-      let us ← elabExplicitUnivs us
-      elabFieldName e field us
+    | `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit
+    | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit
+    | `($(e).$field:ident) => elabFieldName e field explicit
+    | `($e |>.$field:ident) => elabFieldName e field explicit
+    | `(@$(e).$idx:fieldIdx) => elabFieldIdx e idx (explicit := true)
+    | `(@$(e).$field:ident) => elabFieldName e field (explicit := true)
     | `($_:ident@$_:term) =>
       throwError m!"Expected a function, but found the named pattern{indentD f}"
         ++ .note m!"Named patterns `<identifier>@<term>` can only be used when pattern-matching"
@@ -1959,15 +1942,12 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `($id:ident.{$us,*}) => do
       let us ← elabExplicitUnivs us
       elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
-    | `(.$id:ident) => elabDottedIdent id []
+    | `(.$id:ident) => elabDottedIdent id [] explicit
     | `(.$id:ident.{$us,*}) =>
       let us ← elabExplicitUnivs us
-      elabDottedIdent id us
+      elabDottedIdent id us explicit
     | `(@$_:ident)
     | `(@$_:ident.{$_us,*})
-    | `(@$(_).$_:fieldIdx)
-    | `(@$(_).$_:ident)
-    | `(@$(_).$_:ident.{$_us,*})
     | `(@.$_:ident)
     | `(@.$_:ident.{$_us,*}) =>
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
@@ -2104,10 +2084,10 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 @[builtin_term_elab dotIdent] def elabDotIdent : TermElab := elabAtom
 @[builtin_term_elab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
 @[builtin_term_elab pipeProj] def elabPipeProj : TermElab
-  | `($e |>.%$tk$f$[.{$us?,*}]? $args*), expectedType? =>
+  | `($e |>.%$tk$f $args*), expectedType? =>
     universeConstraintsCheckpoint do
       let (namedArgs, args, ellipsis) ← expandArgs args
-      let mut stx ← `($e |>.%$tk$f$[.{$us?,*}]?)
+      let mut stx ← `($e |>.%$tk$f)
       if let (some startPos, some stopPos) := (e.raw.getPos?, f.raw.getTailPos?) then
         stx := ⟨stx.raw.setInfo <| .synthetic (canonical := true) startPos stopPos⟩
       elabAppAux stx namedArgs args (ellipsis := ellipsis) expectedType?
@@ -2115,16 +2095,15 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
   match stx with
-  | `(@$_:ident)               => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
-  | `(@$_:ident.{$_us,*})      => elabAtom stx expectedType?
-  | `(@$(_).$_:fieldIdx)       => elabAtom stx expectedType?
-  | `(@$(_).$_:ident)          => elabAtom stx expectedType?
-  | `(@$(_).$_:ident.{$_us,*}) => elabAtom stx expectedType?
-  | `(@.$_:ident)              => elabAtom stx expectedType?
-  | `(@.$_:ident.{$_us,*})     => elabAtom stx expectedType?
-  | `(@($t))                   => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | `(@$t)                     => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | _                          => throwUnsupportedSyntax
+  | `(@$_:ident)           => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
+  | `(@$_:ident.{$_us,*})  => elabAtom stx expectedType?
+  | `(@$(_).$_:fieldIdx)   => elabAtom stx expectedType?
+  | `(@$(_).$_:ident)      => elabAtom stx expectedType?
+  | `(@.$_:ident)          => elabAtom stx expectedType?
+  | `(@.$_:ident.{$_us,*}) => elabAtom stx expectedType?
+  | `(@($t))               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | `(@$t)                 => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | _                      => throwUnsupportedSyntax
 
 @[builtin_term_elab choice] def elabChoice : TermElab := elabAtom
 @[builtin_term_elab proj] def elabProj : TermElab := elabAtom

src/Lean/Elab/AutoBound.lean

@@ -74,7 +74,7 @@ def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=
 /--
 Tracks extra context needed within the scope of `Lean.Elab.Term.withAutoBoundImplicit`
 -/
-structure AutoBoundImplicitContext where
+public structure AutoBoundImplicitContext where
   /--
   This always matches the `autoImplicit` option; it is duplicated here in
   order to support the behavior of the deprecated `Lean.Elab.Term.Context.autoImplicit`
@@ -95,7 +95,7 @@ instance : EmptyCollection AutoBoundImplicitContext where
 Pushes a new variable onto the autoImplicit context, indicating that it needs
 to be bound as an implicit parameter.
 -/
-def AutoBoundImplicitContext.push (ctx : AutoBoundImplicitContext) (x : Expr) :=
+public def AutoBoundImplicitContext.push (ctx : AutoBoundImplicitContext) (x : Expr) :=
   { ctx with boundVariables := ctx.boundVariables.push x }
 
 end Lean.Elab

src/Lean/Elab/BuiltinCommand.lean

@@ -116,9 +116,8 @@ private def checkEndHeader : Name → List Scope → Option Name
       addScope (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (isMeta := metaTk.isSome) (attrs := attrs) "" (← getCurrNamespace)
   | _                        => throwUnsupportedSyntax
 
-@[builtin_command_elab InternalSyntax.end_local_scope] def elabEndLocalScope : CommandElab := fun stx => do
-  let depth := stx[1].toNat
-  setDelimitsLocal depth
+@[builtin_command_elab InternalSyntax.end_local_scope] def elabEndLocalScope : CommandElab := fun _ => do
+  setDelimitsLocal
 
 /--
 Produces a `Name` composed of the names of at most the innermost `n` scopes in `ss`, truncating if an
@@ -529,7 +528,7 @@ open Lean.Parser.Command.InternalSyntax in
 @[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
   | `($cmd₁ in%$tk $cmd₂) =>
     -- Limit ref variability for incrementality; see Note [Incremental Macros]
-    withRef tk `(section $cmd₁:command $(endLocalScopeSyntax 1):command $cmd₂ end)
+    withRef tk `(section $cmd₁:command $endLocalScopeSyntax:command $cmd₂ end)
   | _                 => Macro.throwUnsupported
 
 @[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do

src/Lean/Elab/BuiltinDo/For.lean

@@ -111,14 +111,8 @@ open Lean.Meta
     for x in loopMutVars do
       let defn ← getLocalDeclFromUserName x.getId
       Term.addTermInfo' x defn.toExpr
-      -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type.
-      -- If we don't do this, then we are stuck on solving constraints such as
-      --   `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47`
-      -- It's important we do this as a separate isLevelDefEq check on the decremented level because
-      -- otherwise (`ensureHasType (mkSort mi.u.succ)`) we are stuck on constraints like
-      --   `max (?u+1) (?v+1) =?= ?u+1`
-      let u ← getDecLevel defn.type
-      discard <| isLevelDefEq u mi.u
+      -- ForIn forces all mut vars into the same universe: that of the do block result type.
+      discard <| Term.ensureHasType (mkSort (mi.u.succ)) defn.type
       defs := defs.push defn.toExpr
     if info.returnsEarly && loopMutVars.isEmpty then
       defs := defs.push (mkConst ``Unit.unit)
@@ -153,9 +147,6 @@ open Lean.Meta
 
   let body ←
     withLocalDeclsD xh fun xh => do
-    Term.addLocalVarInfo x xh[0]!
-    if let some h := h? then
-      Term.addLocalVarInfo h xh[1]!
     withLocalDecl s .default σ (kind := .implDetail) fun loopS => do
     mkLambdaFVars (xh.push loopS) <| ← do
     bindMutVarsFromTuple loopMutVarNames loopS.fvarId! do

src/Lean/Elab/BuiltinTerm.lean

@@ -314,23 +314,6 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     return val
   | _ => panic! "resolveId? returned an unexpected expression"
 
-/--
-Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
-Non-instance-implicit arguments are assigned from the original application's arguments.
-If the function is over-applied, extra arguments are preserved.
--/
-private def resynthInstImplicitArgs (type : Expr) : TermElabM Expr := do
-  let fn := type.getAppFn
-  let args := type.getAppArgs
-  let (mvars, bis, _) ← forallMetaTelescope (← inferType fn)
-  for i in [:mvars.size] do
-    if bis[i]!.isInstImplicit then
-      mvars[i]!.mvarId!.assign (← mkInstMVar (← inferType mvars[i]!))
-    else
-      mvars[i]!.mvarId!.assign args[i]!
-  let args := mvars ++ args.drop mvars.size
-  instantiateMVars (mkAppN fn args)
-
 @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
   -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
   let typeStx := stx[stx.getNumArgs - 1]!
@@ -342,21 +325,19 @@ private def resynthInstImplicitArgs (type : Expr) : TermElabM Expr := do
       .note "`inferInstanceAs` requires full knowledge of the expected (\"target\") type to do its \
         instance translation. If you do not intend to transport instances between two types, \
         consider using `inferInstance` or `(inferInstance : expectedType)` instead.")
-  let type ← withSynthesize do
-    let type ← elabType typeStx
-    -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
-    discard <| isDefEq type expectedType
-    return type
-  -- Re-infer instance-implicit args, so that synthesis is not influenced by the expected type's
-  -- instance choices.
-  let type ← withSynthesize <| resynthInstImplicitArgs type
+  let type ← withSynthesize (postpone := .yes) <| elabType typeStx
+  -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
+  discard <| isDefEq type expectedType
   let type ← instantiateMVars type
+  -- Rebuild type with fresh synthetic mvars for instance-implicit args, so that
+  -- synthesis is not influenced by the expected type's instance choices.
+  let type ← abstractInstImplicitArgs type
   let inst ← synthInstance type
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
     -- Wrap instance so its type matches the expected type exactly.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
     let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
-    wrapInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
+    withNewMCtxDepth <| wrapInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/DeclModifiers.lean

@@ -7,19 +7,11 @@ module
 
 prelude
 public import Lean.DocString.Add
-public import Lean.Linter.Basic
 meta import Lean.Parser.Command
 
 public section
 
-namespace Lean
-
-register_builtin_option linter.redundantVisibility : Bool := {
-  defValue := false
-  descr := "warn on redundant `private`/`public` visibility modifiers"
-}
-
-namespace Elab
+namespace Lean.Elab
 
 /--
 Ensure the environment does not contain a declaration with name `declName`.
@@ -73,44 +65,9 @@ def Visibility.isPublic : Visibility → Bool
   | .public    => true
   | _          => false
 
-/--
-Returns whether the given visibility modifier should be interpreted as `public` in the current
-environment.
-
-NOTE: `Environment.isExporting` defaults to `false` when command elaborators are invoked for
-backward compatibility. It needs to be initialized apropriately first before calling this function
-as e.g. done in `elabDeclaration`.
--/
 def Visibility.isInferredPublic (env : Environment) (v : Visibility) : Bool :=
   if env.isExporting || !env.header.isModule then !v.isPrivate else v.isPublic
 
-/-- Converts optional visibility syntax to a `Visibility` value. -/
-def elabVisibility [Monad m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m]
-    [AddMessageContext m]
-    (vis? : Option (TSyntax ``Parser.Command.visibility)) :
-    m Visibility := do
-  let env ← getEnv
-  match vis? with
-  | none   => pure .regular
-  | some v =>
-    match v with
-    | `(Parser.Command.visibility| private) =>
-      if v.raw.getHeadInfo matches .original .. then  -- skip macro output
-        if env.header.isModule && !env.isExporting then
-          Linter.logLintIf linter.redundantVisibility v
-            m!"`private` has no effect in a `module` file outside `public section`; \
-            declarations are already `private` by default"
-      pure .private
-    | `(Parser.Command.visibility| public) =>
-      if v.raw.getHeadInfo matches .original .. then  -- skip macro output
-        if env.isExporting || !env.header.isModule then
-          Linter.logLintIf linter.redundantVisibility v
-            m!"`public` is the default visibility{
-              if env.header.isModule then " inside a `public section`" else ""
-            }; the modifier has no effect"
-      pure .public
-    | _ => throwErrorAt v "unexpected visibility modifier"
-
 /-- Whether a declaration is default, partial or nonrec. -/
 inductive RecKind where
   | «partial» | «nonrec» | default
@@ -226,7 +183,13 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
     else
       RecKind.nonrec
   let docString? := docCommentStx.getOptional?.map (TSyntax.mk ·, doc.verso.get (← getOptions))
-  let visibility ← elabVisibility (visibilityStx.getOptional?.map (⟨·⟩))
+  let visibility ← match visibilityStx.getOptional? with
+    | none   => pure .regular
+    | some v =>
+      match v with
+      | `(Parser.Command.visibility| private) => pure .private
+      | `(Parser.Command.visibility| public) => pure .public
+      | _ => throwErrorAt v "unexpected visibility modifier"
   let isProtected := !protectedStx.isNone
   let attrs ← match attrsStx.getOptional? with
     | none       => pure #[]

src/Lean/Elab/Declaration.lean

@@ -152,9 +152,8 @@ def expandNamespacedDeclaration : Macro := fun stx => do
   | some (ns, newStx) => do
     -- Limit ref variability for incrementality; see Note [Incremental Macros]
     let declTk := stx[1][0]
-    let depth := ns.getNumParts
     let ns := mkIdentFrom declTk ns
-    withRef declTk `(namespace $ns $(endLocalScopeSyntax depth):command $(⟨newStx⟩) end $ns)
+    withRef declTk `(namespace $ns $endLocalScopeSyntax:command $(⟨newStx⟩) end $ns)
   | none => Macro.throwUnsupported
 
 @[builtin_command_elab declaration, builtin_incremental]
@@ -341,29 +340,31 @@ def elabMutual : CommandElab := fun stx => do
 
 @[builtin_command_elab Lean.Parser.Command.«initialize»] def elabInitialize : CommandElab
   | stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ←]? $doSeq) => do
-    withExporting (isExporting := (← getScope).isPublic) do
     let attrId := mkIdentFrom stx <| if kw.raw[0].isToken "initialize" then `init else `builtin_init
     if let (some id, some type) := (id?, type?) then
       let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(vis?)? $[meta%$meta?]? $[unsafe%$unsafe?]?) := stx[0]
         | throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
       let defStx ← `($[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? $[meta%$meta?]? opaque $id : $type)
       let mut fullId := (← getCurrNamespace) ++ id.getId
-      let visibility ← elabVisibility vis?
-      if !visibility.isInferredPublic (← getEnv) then
+      if vis?.any (·.raw.isOfKind ``Parser.Command.private) then
         fullId := mkPrivateName (← getEnv) fullId
       -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
       -- otherwise the info context created by `with_decl_name` will be incomplete and break the
       -- call hierarchy
       addDeclarationRangesForBuiltin fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
+      let vis := Parser.Command.visibility.ofBool (!isPrivateName fullId)
       elabCommand (← `(
-        @[no_expose] private $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
+        $vis:visibility $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
         $defStx:command))
     else
       let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(_)? $[meta%$meta?]? $[unsafe%$unsafe?]?) := declModifiers
         | throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
       let attrs := (attrs?.map (·.getElems)).getD #[]
       let attrs := attrs.push (← `(Lean.Parser.Term.attrInstance| $attrId:ident))
-      elabCommand (← `($[$doc?:docComment]? @[no_expose, $[$attrs],*] private $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO Unit := do $doSeq))
+      -- `[builtin_init]` can be private as it is used for local codegen only but `[init]` must be
+      -- available for the interpreter.
+      let vis := Parser.Command.visibility.ofBool (attrId.getId == `init)
+      elabCommand (← `($[$doc?:docComment]? @[$[$attrs],*] $vis:visibility $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO Unit := do $doSeq))
   | _ => throwUnsupportedSyntax
 
 builtin_initialize

src/Lean/Elab/Deriving/BEq.lean

@@ -172,7 +172,7 @@ def mkMatchNew (header : Header) (indVal : InductiveVal) (auxFunName : Name) : T
   if indVal.numCtors == 1 then
     `( $(mkCIdent casesOnSameCtorName) $x1:term $x2:term rfl $alts:term* )
   else
-    `( match Nat.decEq ($(mkCIdent ctorIdxName) $x1:ident) ($(mkCIdent ctorIdxName) $x2:ident) with
+    `( match decEq ($(mkCIdent ctorIdxName) $x1:ident) ($(mkCIdent ctorIdxName) $x2:ident) with
       | .isTrue h => $(mkCIdent casesOnSameCtorName) $x1:term $x2:term h $alts:term*
       | .isFalse _ => false)
 

src/Lean/Elab/Deriving/Inhabited.lean

@@ -25,23 +25,25 @@ private def mkInhabitedInstanceUsing (inductiveTypeName : Name) (ctorName : Name
   | none =>
     return false
 where
-  addLocalInstancesForParamsAux {α} (k : Array Expr → LocalInst2Index → TermElabM α) : List Expr → Nat → Array Expr → LocalInst2Index → TermElabM α
-    | [],    _, insts, map => k insts map
-    | x::xs, i, insts, map =>
+  addLocalInstancesForParamsAux {α} (k : LocalInst2Index → TermElabM α) : List Expr → Nat → LocalInst2Index → TermElabM α
+    | [], _, map    => k map
+    | x::xs, i, map =>
       try
         let instType ← mkAppM `Inhabited #[x]
-        check instType
-        withLocalDecl (← mkFreshUserName `inst) .instImplicit instType fun inst => do
-          trace[Elab.Deriving.inhabited] "adding local instance {instType}"
-          addLocalInstancesForParamsAux k xs (i+1) (insts.push inst) (map.insert inst.fvarId! i)
+        if (← isTypeCorrect instType) then
+          withLocalDeclD (← mkFreshUserName `inst) instType fun inst => do
+            trace[Elab.Deriving.inhabited] "adding local instance {instType}"
+            addLocalInstancesForParamsAux k xs (i+1) (map.insert inst.fvarId! i)
+        else
+          addLocalInstancesForParamsAux k xs (i+1) map
       catch _ =>
-        addLocalInstancesForParamsAux k xs (i+1) insts map
+        addLocalInstancesForParamsAux k xs (i+1) map
 
-  addLocalInstancesForParams {α} (xs : Array Expr) (k : Array Expr → LocalInst2Index → TermElabM α) : TermElabM α := do
+  addLocalInstancesForParams {α} (xs : Array Expr) (k : LocalInst2Index → TermElabM α) : TermElabM α := do
     if addHypotheses then
-      addLocalInstancesForParamsAux k xs.toList 0 #[] {}
+      addLocalInstancesForParamsAux k xs.toList 0 {}
     else
-      k #[] {}
+      k {}
 
   collectUsedLocalsInsts (usedInstIdxs : IndexSet) (localInst2Index : LocalInst2Index) (e : Expr) : IndexSet :=
     if localInst2Index.isEmpty then
@@ -56,88 +58,58 @@ where
       runST (fun _ => visit |>.run usedInstIdxs) |>.2
 
   /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters
-     at position `i` and `i ∈ usedInstIdxs`. -/
-  mkInstanceCmdWith (instId : Ident) (usedInstIdxs : IndexSet) (auxFunId : Ident) : TermElabM Syntax := do
+     at position `i` and `i ∈ assumingParamIdxs`. -/
+  mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do
+    let ctx ← Deriving.mkContext ``Inhabited "inhabited" inductiveTypeName
     let indVal ← getConstInfoInduct inductiveTypeName
+    let ctorVal ← getConstInfoCtor ctorName
     let mut indArgs := #[]
     let mut binders := #[]
     for i in *...indVal.numParams + indVal.numIndices do
       let arg := mkIdent (← mkFreshUserName `a)
       indArgs := indArgs.push arg
-      binders := binders.push <| ← `(bracketedBinderF| { $arg:ident })
-      if usedInstIdxs.contains i then
-        binders := binders.push <| ← `(bracketedBinderF| [Inhabited $arg:ident ])
+      let binder ← `(bracketedBinderF| { $arg:ident })
+      binders := binders.push binder
+      if assumingParamIdxs.contains i then
+        let binder ← `(bracketedBinderF| [Inhabited $arg:ident ])
+        binders := binders.push binder
     let type ← `(@$(mkCIdent inductiveTypeName):ident $indArgs:ident*)
-    `(instance $instId:ident $binders:bracketedBinder* : Inhabited $type := ⟨$auxFunId⟩)
+    let mut ctorArgs := #[]
+    for _ in *...ctorVal.numParams do
+      ctorArgs := ctorArgs.push (← `(_))
+    for _ in *...ctorVal.numFields do
+      ctorArgs := ctorArgs.push (← ``(Inhabited.default))
+    let val ← `(@$(mkIdent ctorName):ident $ctorArgs*)
+    let ctx ← mkContext ``Inhabited "default" inductiveTypeName
+    let auxFunName := ctx.auxFunNames[0]!
+    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type := $val
+      instance $(mkIdent ctx.instName):ident $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩)
 
-  solveMVarsWithDefault (e : Expr) : TermElabM Unit := do
-    let mvarIds ← getMVarsNoDelayed e
-    mvarIds.forM fun mvarId => mvarId.withContext do
-      unless ← mvarId.isAssigned do
-        let type ← mvarId.getType
-        withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"synthesizing Inhabited instance for{inlineExprTrailing type}") do
-          let val ← mkDefault type
-          mvarId.assign val
-          trace[Elab.Deriving.inhabited] "value:{inlineExprTrailing val}"
 
-  mkDefaultValue (indVal : InductiveVal) : TermElabM (Expr × Expr × IndexSet) := do
-    let us := indVal.levelParams.map Level.param
-    forallTelescopeReducing indVal.type fun xs _ =>
-    withImplicitBinderInfos xs do
-    addLocalInstancesForParams xs[0...indVal.numParams] fun insts localInst2Index => do
-      let type := mkAppN (.const inductiveTypeName us) xs
-      let val ←
-        if isStructure (← getEnv) inductiveTypeName then
-          withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using structure instance elaborator") do
-            let stx ← `(structInstDefault| struct_inst_default%)
-            withoutErrToSorry <| elabTermAndSynthesize stx type
-        else
-          withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using constructor `{.ofConstName ctorName}`") do
-            let val := mkAppN (.const ctorName us) xs[0...indVal.numParams]
-            let (mvars, _, type') ← forallMetaTelescopeReducing (← inferType val)
-            unless ← isDefEq type type' do
-              throwError "cannot unify{indentExpr type}\nand type of constructor{indentExpr type'}"
-            pure <| mkAppN val mvars
-      solveMVarsWithDefault val
-      let val ← instantiateMVars val
-      if val.hasMVar then
-        throwError "default value contains metavariables{inlineExprTrailing val}"
-      let fvars := Lean.collectFVars {} val
-      let insts' := insts.filter fvars.visitedExpr.contains
-      let usedInstIdxs := collectUsedLocalsInsts {} localInst2Index val
-      assert! insts'.size == usedInstIdxs.size
-      trace[Elab.Deriving.inhabited] "inhabited instance using{inlineExpr val}{if insts'.isEmpty then m!"" else m!"(assuming parameters {insts'} are inhabited)"}"
-      let xs' := xs ++ insts'
-      let auxType ← mkForallFVars xs' type
-      let auxVal ← mkLambdaFVars xs' val
-      return (auxType, auxVal, usedInstIdxs)
-
-  mkInstanceCmd? : TermElabM (Option Syntax) :=
-    withExporting (isExporting := !isPrivateName ctorName) do
-      let ctx ← mkContext ``Inhabited "default" inductiveTypeName
-      let auxFunName := (← getCurrNamespace) ++ ctx.auxFunNames[0]!
-      let indVal ← getConstInfoInduct inductiveTypeName
-      let (auxType, auxVal, usedInstIdxs) ←
-        try
-          withDeclName auxFunName do mkDefaultValue indVal
-        catch e =>
-          trace[Elab.Deriving.inhabited] "error: {e.toMessageData}"
+  mkInstanceCmd? : TermElabM (Option Syntax) := do
+    let ctorVal ← getConstInfoCtor ctorName
+    forallTelescopeReducing ctorVal.type fun xs _ =>
+      addLocalInstancesForParams xs[*...ctorVal.numParams] fun localInst2Index => do
+        let mut usedInstIdxs := {}
+        let mut ok := true
+        for h : i in ctorVal.numParams...xs.size do
+          let x := xs[i]
+          let instType ← mkAppM `Inhabited #[(← inferType x)]
+          trace[Elab.Deriving.inhabited] "checking {instType} for `{ctorName}`"
+          match (← trySynthInstance instType) with
+          | LOption.some e =>
+            usedInstIdxs := collectUsedLocalsInsts usedInstIdxs localInst2Index e
+          | _ =>
+            trace[Elab.Deriving.inhabited] "failed to generate instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
+            ok := false
+            break
+        if !ok then
           return none
-      addDecl <| .defnDecl <| ← mkDefinitionValInferringUnsafe
-        (name        := auxFunName)
-        (levelParams := indVal.levelParams)
-        (type        := auxType)
-        (value       := auxVal)
-        (hints       := ReducibilityHints.regular (getMaxHeight (← getEnv) auxVal + 1))
-      if isMarkedMeta (← getEnv) inductiveTypeName then
-        modifyEnv (markMeta · auxFunName)
-      unless (← read).isNoncomputableSection do
-        compileDecls #[auxFunName]
-      enableRealizationsForConst auxFunName
-      trace[Elab.Deriving.inhabited] "defined {.ofConstName auxFunName}"
-      let cmd ← mkInstanceCmdWith (mkIdent ctx.instName) usedInstIdxs (mkCIdent auxFunName)
-      trace[Elab.Deriving.inhabited] "\n{cmd}"
-      return some cmd
+        else
+          trace[Elab.Deriving.inhabited] "inhabited instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}"
+          let cmd ← mkInstanceCmdWith usedInstIdxs
+          trace[Elab.Deriving.inhabited] "\n{cmd}"
+          return some cmd
 
 private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do
   withoutExposeFromCtors declName do

src/Lean/Elab/Do/Basic.lean

@@ -384,7 +384,6 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
   let k := dec.k
   -- The .ofBinderName below is mainly to interpret `__do_lift` binders as implementation details.
   let declKind := .ofBinderName x
-  let kResultTy ← mkFreshResultType `kResultTy
   withLocalDecl x .default eResultTy (kind := declKind) fun xFVar => do
     let body ← k
     let body' := body.consumeMData
@@ -412,6 +411,7 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
         -- else -- would be too aggressive
         --   return ← mapLetDecl (nondep := true) (kind := declKind) x eResultTy eRes fun _ => k ref
 
+    let kResultTy ← mkFreshResultType `kResultTy
     let body ← Term.ensureHasType (← mkMonadicType kResultTy) body
     let k ← mkLambdaFVars #[xFVar] body
     mkBindApp eResultTy kResultTy e k
@@ -545,10 +545,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
-  unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
-    joinRhsMVar.mvarId!.withContext do
-      throwError "Bug in a `do` elaborator. Failed to assign join point RHS{indentExpr joinRhs}\n\
-        to metavariable\n{joinRhsMVar.mvarId!}"
+  discard <| joinRhsMVar.mvarId!.checkedAssign joinRhs
 
   let body ← body?.getDM do
     -- Here we unconditionally add a pending MVar.

src/Lean/Elab/Do/Legacy.lean

@@ -1782,10 +1782,6 @@ mutual
             doIfToCode doElem doElems
           else if k == ``Parser.Term.doUnless then
             doUnlessToCode doElem doElems
-          else if k == `Lean.doRepeat then
-            let seq := doElem[1]
-            let expanded ← `(doElem| for _ in Loop.mk do $seq)
-            doSeqToCode (expanded :: doElems)
           else if k == ``Parser.Term.doFor then withFreshMacroScope do
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then

src/Lean/Elab/DocString.lean

@@ -1038,19 +1038,19 @@ builtin_initialize registerBuiltinAttribute {
 }
 end
 
-unsafe def codeSuggestionsUnsafe : TermElabM (Array (StrLit → DocM (Array CodeSuggestion))) := do
+private unsafe def codeSuggestionsUnsafe : TermElabM (Array (StrLit → DocM (Array CodeSuggestion))) := do
   let names := (codeSuggestionExt.getState (← getEnv)) |>.toArray
   return (← names.mapM (evalConst _)) ++ (← builtinCodeSuggestions.get).map (·.2)
 
 @[implemented_by codeSuggestionsUnsafe]
-opaque codeSuggestions : TermElabM (Array (StrLit → DocM (Array CodeSuggestion)))
+private opaque codeSuggestions : TermElabM (Array (StrLit → DocM (Array CodeSuggestion)))
 
-unsafe def codeBlockSuggestionsUnsafe : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion))) := do
+private unsafe def codeBlockSuggestionsUnsafe : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion))) := do
   let names := (codeBlockSuggestionExt.getState (← getEnv)) |>.toArray
   return (← names.mapM (evalConst _)) ++ (← builtinCodeBlockSuggestions.get).map (·.2)
 
 @[implemented_by codeBlockSuggestionsUnsafe]
-opaque codeBlockSuggestions : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion)))
+private opaque codeBlockSuggestions : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion)))
 
 /--
 Resolves a name against `NameMap` that contains a list of builtin expanders, taking into account
@@ -1060,7 +1060,7 @@ resolution (`realizeGlobalConstNoOverload`) won't find them.
 
 This is called as a fallback when the identifier can't be resolved.
 -/
-def resolveBuiltinDocName {α : Type} (builtins : NameMap α) (x : Name) : TermElabM (Option α) := do
+private def resolveBuiltinDocName {α : Type} (builtins : NameMap α) (x : Name) : TermElabM (Option α) := do
   if let some v := builtins.get? x then return some v
 
   -- Builtins shouldn't require a prefix, as they're part of the language.
@@ -1089,7 +1089,7 @@ def resolveBuiltinDocName {α : Type} (builtins : NameMap α) (x : Name) : TermE
 
   return none
 
-unsafe def roleExpandersForUnsafe (roleName : Ident) :
+private unsafe def roleExpandersForUnsafe (roleName : Ident) :
     TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)))) := do
   let x? ←
     try some <$> realizeGlobalConstNoOverload roleName
@@ -1105,10 +1105,10 @@ unsafe def roleExpandersForUnsafe (roleName : Ident) :
 
 
 @[implemented_by roleExpandersForUnsafe]
-opaque roleExpandersFor (roleName : Ident) :
+private opaque roleExpandersFor (roleName : Ident) :
   TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline))))
 
-unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
+private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
     TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
   let x? ←
     try some <$> realizeGlobalConstNoOverload codeBlockName
@@ -1124,10 +1124,10 @@ unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
 
 
 @[implemented_by codeBlockExpandersForUnsafe]
-opaque codeBlockExpandersFor (codeBlockName : Ident) :
+private opaque codeBlockExpandersFor (codeBlockName : Ident) :
   TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
 
-unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
+private unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
     TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
   let x? ←
     try some <$> realizeGlobalConstNoOverload directiveName
@@ -1142,10 +1142,10 @@ unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
     return hasBuiltin.toArray.flatten
 
 @[implemented_by directiveExpandersForUnsafe]
-opaque directiveExpandersFor (directiveName : Ident) :
+private opaque directiveExpandersFor (directiveName : Ident) :
   TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
 
-unsafe def commandExpandersForUnsafe (commandName : Ident) :
+private unsafe def commandExpandersForUnsafe (commandName : Ident) :
     TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
   let x? ←
     try some <$> realizeGlobalConstNoOverload commandName
@@ -1161,18 +1161,18 @@ unsafe def commandExpandersForUnsafe (commandName : Ident) :
     return hasBuiltin.toArray.flatten
 
 @[implemented_by commandExpandersForUnsafe]
-opaque commandExpandersFor (commandName : Ident) :
+private opaque commandExpandersFor (commandName : Ident) :
   TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
 
 
-def mkArgVal (arg : TSyntax `arg_val) : DocM Term :=
+private def mkArgVal (arg : TSyntax `arg_val) : DocM Term :=
   match arg with
   | `(arg_val|$n:ident) => pure n
   | `(arg_val|$n:num) => pure n
   | `(arg_val|$s:str) => pure s
   | _ => throwErrorAt arg "Didn't understand as argument value"
 
-def mkArg (arg : TSyntax `doc_arg) : DocM (TSyntax ``Parser.Term.argument) := do
+private def mkArg (arg : TSyntax `doc_arg) : DocM (TSyntax ``Parser.Term.argument) := do
   match arg with
   | `(doc_arg|$x:arg_val) =>
     let x ← mkArgVal x
@@ -1190,7 +1190,7 @@ def mkArg (arg : TSyntax `doc_arg) : DocM (TSyntax ``Parser.Term.argument) := do
     `(Parser.Term.argument| ($x := $v))
   | _ => throwErrorAt arg "Didn't understand as argument"
 
-def mkAppStx (name : Ident) (args : TSyntaxArray `doc_arg) : DocM Term := do
+private def mkAppStx (name : Ident) (args : TSyntaxArray `doc_arg) : DocM Term := do
   return ⟨mkNode ``Parser.Term.app #[name, mkNullNode (← args.mapM mkArg)]⟩
 
 /--
@@ -1204,7 +1204,7 @@ register_builtin_option doc.verso.suggestions : Bool := {
 -- Normally, name suggestions should be provided relative to the current scope. But
 -- during bootstrapping, the names in question may not yet be defined, so builtin
 -- names need special handling.
-def suggestionName (name : Name) : TermElabM Name := do
+private def suggestionName (name : Name) : TermElabM Name := do
   let name' ←
     -- Builtin expander names never need namespacing
     if (← builtinDocRoles.get).contains name then pure (some name)
@@ -1241,7 +1241,7 @@ def suggestionName (name : Name) : TermElabM Name := do
         -- Fall back to doing nothing
         pure name
 
-def sortSuggestions (ss : Array Meta.Hint.Suggestion) : Array Meta.Hint.Suggestion :=
+private def sortSuggestions (ss : Array Meta.Hint.Suggestion) : Array Meta.Hint.Suggestion :=
   let cmp : (x y : Meta.Tactic.TryThis.SuggestionText) → Bool
     | .string s1, .string s2 => s1 < s2
     | .string _, _ => true
@@ -1250,7 +1250,7 @@ def sortSuggestions (ss : Array Meta.Hint.Suggestion) : Array Meta.Hint.Suggesti
   ss.qsort (cmp ·.suggestion ·.suggestion)
 
 open Diff in
-def mkSuggestion
+private def mkSuggestion
     (ref : Syntax) (hintTitle : MessageData)
     (newStrings : Array (String × Option String × Option String)) :
     DocM MessageData := do
@@ -1281,7 +1281,7 @@ def nameOrBuiltinName [Monad m] [MonadEnv m] (x : Name) : m Name := do
 Finds registered expander names that `x` is a suffix of, for use in error message hints when the
 name is shadowed. Returns display names suitable for `mkSuggestion`.
 -/
-def findShadowedNames {α : Type}
+private def findShadowedNames {α : Type}
     (nonBuiltIns : NameMap (Array Name)) (builtins : NameMap α) (x : Name) :
     TermElabM (Array Name) := do
   if x.isAnonymous then return #[]
@@ -1303,7 +1303,7 @@ def findShadowedNames {α : Type}
 /--
 Builds a hint for an "Unknown role/directive/..." error when the name might be shadowed.
 -/
-def shadowedHint {α : Type}
+private def shadowedHint {α : Type}
     (envEntries : NameMap (Array Name)) (builtins : NameMap α)
     (name : Ident) (kind : String) : DocM MessageData := do
   let candidates ← findShadowedNames envEntries builtins name.getId
@@ -1316,7 +1316,7 @@ Throws an appropriate error for an unknown doc element (role/directive/code bloc
 Distinguishes "name resolves but isn't registered" from "name doesn't resolve at all",
 and includes shadowed-name suggestions when applicable.
 -/
-def throwUnknownDocElem {α β : Type}
+private def throwUnknownDocElem {α β : Type}
     (envEntries : NameMap (Array Name)) (builtins : NameMap α)
     (name : Ident) (kind : String) : DocM β := do
   let hint ← shadowedHint envEntries builtins name kind
@@ -1545,12 +1545,12 @@ where
   withSpace (s : String) : String :=
     if s.endsWith " " then s else s ++ " "
 
-def takeFirst? (xs : Array α) : Option (α × Array α) :=
+private def takeFirst? (xs : Array α) : Option (α × Array α) :=
   if h : xs.size > 0 then
     some (xs[0], xs.extract 1)
   else none
 
-partial def elabBlocks' (level : Nat) :
+private partial def elabBlocks' (level : Nat) :
     StateT (TSyntaxArray `block) DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) := do
   let mut pre := #[]
   let mut sub := #[]
@@ -1586,7 +1586,7 @@ partial def elabBlocks' (level : Nat) :
       break
   return (pre, sub)
 
-def elabModSnippet'
+private def elabModSnippet'
     (range : DeclarationRange) (level : Nat) (blocks : TSyntaxArray `block) :
     DocM VersoModuleDocs.Snippet := do
   let mut snippet : VersoModuleDocs.Snippet := {
@@ -1616,7 +1616,7 @@ def elabModSnippet'
         snippet := snippet.addBlock (← elabBlock b)
   return snippet
 
-partial def fixupInline (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
+private partial def fixupInline (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
   match inl with
   | .concat xs => .concat <$> xs.mapM fixupInline
   | .emph xs => .emph <$> xs.mapM fixupInline
@@ -1663,7 +1663,7 @@ partial def fixupInline (inl : Inline ElabInline) : DocM (Inline ElabInline) :=
         return .empty
     | _ => .other i <$> xs.mapM fixupInline
 
-partial def fixupBlock (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
+private partial def fixupBlock (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
   match block with
   | .para xs => .para <$> xs.mapM fixupInline
   | .concat xs => .concat <$> xs.mapM fixupBlock
@@ -1677,7 +1677,7 @@ partial def fixupBlock (block : Block ElabInline ElabBlock) : DocM (Block ElabIn
   | .code s => pure (.code s)
   | .other i xs => .other i <$> xs.mapM fixupBlock
 
-partial def fixupPart (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
+private partial def fixupPart (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
   return { part with
     title := ← part.title.mapM fixupInline
     content := ← part.content.mapM fixupBlock,
@@ -1685,13 +1685,13 @@ partial def fixupPart (part : Part ElabInline ElabBlock Empty) : DocM (Part Elab
   }
 
 
-partial def fixupBlocks : (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) → DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty))
+private partial def fixupBlocks : (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) → DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty))
   | (bs, ps) => do
     let bs ← bs.mapM fixupBlock
     let ps ← ps.mapM fixupPart
     return (bs, ps)
 
-partial def fixupSnippet (snippet : VersoModuleDocs.Snippet) : DocM VersoModuleDocs.Snippet := do
+private partial def fixupSnippet (snippet : VersoModuleDocs.Snippet) : DocM VersoModuleDocs.Snippet := do
   return {snippet with
     text := ← snippet.text.mapM fixupBlock,
     sections := ← snippet.sections.mapM fun (level, range, content) => do
@@ -1700,7 +1700,7 @@ partial def fixupSnippet (snippet : VersoModuleDocs.Snippet) : DocM VersoModuleD
 /--
 After fixing up the references, check to see which were not used and emit a suitable warning.
 -/
-def warnUnusedRefs : DocM Unit := do
+private def warnUnusedRefs : DocM Unit := do
   for (_, {location, seen, ..}) in (← getThe InternalState).urls do
     unless seen do
       logWarningAt location "Unused URL"

src/Lean/Elab/DocString/Builtin/Keywords.lean

@@ -31,7 +31,7 @@ structure Data.Atom where
 deriving TypeName
 
 
-def onlyCode [Monad m] [MonadError m] (xs : TSyntaxArray `inline) : m StrLit := do
+private def onlyCode [Monad m] [MonadError m] (xs : TSyntaxArray `inline) : m StrLit := do
   if h : xs.size = 1 then
     match xs[0] with
     | `(inline|code($s)) => return s
@@ -43,7 +43,7 @@ def onlyCode [Monad m] [MonadError m] (xs : TSyntaxArray `inline) : m StrLit :=
 /--
 Checks whether a syntax descriptor's value contains the given atom.
 -/
-partial def containsAtom (e : Expr) (atom : String) : MetaM Bool := do
+private partial def containsAtom (e : Expr) (atom : String) : MetaM Bool := do
   let rec attempt (p : Expr) (tryWhnf : Bool) : MetaM Bool := do
     match p.getAppFnArgs with
     | (``ParserDescr.node, #[_, _, p]) => containsAtom p atom
@@ -67,7 +67,7 @@ partial def containsAtom (e : Expr) (atom : String) : MetaM Bool := do
 Checks whether a syntax descriptor's value contains the given atom. If so, the residual value after
 the atom is returned.
 -/
-partial def containsAtom' (e : Expr) (atom : String) : MetaM (Option Expr) := do
+private partial def containsAtom' (e : Expr) (atom : String) : MetaM (Option Expr) := do
   let rec attempt (p : Expr) (tryWhnf : Bool) : MetaM (Option Expr) := do
     match p.getAppFnArgs with
     | (``ParserDescr.node, #[_, _, p]) => containsAtom' p atom
@@ -92,7 +92,7 @@ partial def containsAtom' (e : Expr) (atom : String) : MetaM (Option Expr) := do
     | _ => if tryWhnf then attempt (← Meta.whnf p) false else pure none
   attempt e true
 
-partial def canEpsilon (e : Expr) : MetaM Bool := do
+private partial def canEpsilon (e : Expr) : MetaM Bool := do
   let rec attempt (p : Expr) (tryWhnf : Bool) : MetaM Bool := do
     match p.getAppFnArgs with
     | (``ParserDescr.node, #[_, _, p]) => canEpsilon p
@@ -118,7 +118,7 @@ partial def canEpsilon (e : Expr) : MetaM Bool := do
 Checks whether a syntax descriptor's value begins with the given atom. If so, the residual value
 after the atom is returned.
 -/
-partial def startsWithAtom? (e : Expr) (atom : String) : MetaM (Option Expr) := do
+private partial def startsWithAtom? (e : Expr) (atom : String) : MetaM (Option Expr) := do
   let rec attempt (p : Expr) (tryWhnf : Bool) : MetaM (Option Expr) := do
     match p.getAppFnArgs with
     | (``ParserDescr.node, #[_, _, p]) => startsWithAtom? p atom
@@ -149,7 +149,7 @@ partial def startsWithAtom? (e : Expr) (atom : String) : MetaM (Option Expr) :=
 Checks whether a syntax descriptor's value begins with the given atoms. If so, the residual value
 after the atoms is returned.
 -/
-partial def startsWithAtoms? (e : Expr) (atoms : List String) : MetaM (Option Expr) := do
+private partial def startsWithAtoms? (e : Expr) (atoms : List String) : MetaM (Option Expr) := do
   match atoms with
   | [] => pure e
   | a :: as =>
@@ -157,7 +157,7 @@ partial def startsWithAtoms? (e : Expr) (atoms : List String) : MetaM (Option Ex
       startsWithAtoms? e' as
     else pure none
 
-partial def exprContainsAtoms (e : Expr) (atoms : List String) : MetaM Bool := do
+private partial def exprContainsAtoms (e : Expr) (atoms : List String) : MetaM Bool := do
   match atoms with
   | [] => pure true
   | a :: as =>
@@ -165,7 +165,7 @@ partial def exprContainsAtoms (e : Expr) (atoms : List String) : MetaM Bool := d
       (startsWithAtoms? e' as <&> Option.isSome) <||> exprContainsAtoms e' (a :: as)
     else pure false
 
-def withAtom (cat : Name) (atom : String) : DocM (Array Name) := do
+private def withAtom (cat : Name) (atom : String) : DocM (Array Name) := do
   let env ← getEnv
   let some catContents := (Lean.Parser.parserExtension.getState env).categories.find? cat
     | return #[]
@@ -177,7 +177,7 @@ def withAtom (cat : Name) (atom : String) : DocM (Array Name) := do
         found := found.push k
   return found
 
-partial def isAtoms (atoms : List String) (stx : Syntax) : Bool :=
+private partial def isAtoms (atoms : List String) (stx : Syntax) : Bool :=
   StateT.run (go [stx]) atoms |>.fst
 where
   go (stxs : List Syntax) : StateM (List String) Bool := do
@@ -196,7 +196,7 @@ where
       | .node _ _ args :: ss =>
         go (args.toList ++ ss)
 
-def parserHasAtomPrefix (atoms : List String) (p : Parser) : TermElabM Bool := do
+private def parserHasAtomPrefix (atoms : List String) (p : Parser) : TermElabM Bool := do
   let str := " ".intercalate atoms
   let env ← getEnv
   let options ← getOptions
@@ -206,16 +206,16 @@ def parserHasAtomPrefix (atoms : List String) (p : Parser) : TermElabM Bool := d
   let s := p.fn.run {inputString := str, fileName := "", fileMap := FileMap.ofString str} {env, options} (getTokenTable env) s
   return isAtoms atoms (mkNullNode (s.stxStack.extract 1 s.stxStack.size))
 
-unsafe def namedParserHasAtomPrefixUnsafe (atoms : List String) (parserName : Name) : TermElabM Bool := do
+private unsafe def namedParserHasAtomPrefixUnsafe (atoms : List String) (parserName : Name) : TermElabM Bool := do
   try
     let p ← evalConstCheck Parser ``Parser parserName
     parserHasAtomPrefix atoms p
   catch | _ => pure false
 
 @[implemented_by namedParserHasAtomPrefixUnsafe]
-opaque namedParserHasAtomPrefix (atoms : List String) (parserName : Name) : TermElabM Bool
+private opaque namedParserHasAtomPrefix (atoms : List String) (parserName : Name) : TermElabM Bool
 
-def parserDescrCanEps : ParserDescr → Bool
+private def parserDescrCanEps : ParserDescr → Bool
   | .node _ _ p | .trailingNode _ _ _ p => parserDescrCanEps p
   | .binary ``Parser.andthen p1 p2 => parserDescrCanEps p1 && parserDescrCanEps p2
   | .binary ``Parser.orelse p1 p2 => parserDescrCanEps p1 || parserDescrCanEps p2
@@ -227,7 +227,7 @@ def parserDescrCanEps : ParserDescr → Bool
   | .const ``Parser.ppHardSpace => true
   | _ => false
 
-def parserDescrHasAtom (atom : String) (p : ParserDescr) : TermElabM (Option ParserDescr) := do
+private def parserDescrHasAtom (atom : String) (p : ParserDescr) : TermElabM (Option ParserDescr) := do
   match p with
   | .node _ _ p | .trailingNode _ _ _ p | .unary _ p =>
     parserDescrHasAtom atom p
@@ -249,7 +249,7 @@ def parserDescrHasAtom (atom : String) (p : ParserDescr) : TermElabM (Option Par
     | none, none => pure none
   | _ => pure none
 
-def parserDescrStartsWithAtom (atom : String) (p : ParserDescr) : TermElabM (Option ParserDescr) := do
+private def parserDescrStartsWithAtom (atom : String) (p : ParserDescr) : TermElabM (Option ParserDescr) := do
   match p with
   | .node _ _ p | .trailingNode _ _ _ p | .unary _ p =>
     parserDescrStartsWithAtom atom p
@@ -272,7 +272,7 @@ def parserDescrStartsWithAtom (atom : String) (p : ParserDescr) : TermElabM (Opt
     | none, none => pure none
   | _ => pure none
 
-def parserDescrStartsWithAtoms (atoms : List String) (p : ParserDescr) : TermElabM Bool := do
+private def parserDescrStartsWithAtoms (atoms : List String) (p : ParserDescr) : TermElabM Bool := do
   match atoms with
   | [] => pure true
   | a :: as =>
@@ -280,7 +280,7 @@ def parserDescrStartsWithAtoms (atoms : List String) (p : ParserDescr) : TermEla
       parserDescrStartsWithAtoms as p'
     else pure false
 
-partial def parserDescrHasAtoms (atoms : List String) (p : ParserDescr) : TermElabM Bool := do
+private partial def parserDescrHasAtoms (atoms : List String) (p : ParserDescr) : TermElabM Bool := do
   match atoms with
   | [] => pure true
   | a :: as =>
@@ -289,16 +289,16 @@ partial def parserDescrHasAtoms (atoms : List String) (p : ParserDescr) : TermEl
       else parserDescrHasAtoms (a :: as) p'
     else pure false
 
-unsafe def parserDescrNameHasAtomsUnsafe (atoms : List String) (p : Name) : TermElabM Bool := do
+private unsafe def parserDescrNameHasAtomsUnsafe (atoms : List String) (p : Name) : TermElabM Bool := do
   try
     let p ← evalConstCheck ParserDescr ``ParserDescr p
     parserDescrHasAtoms atoms p
   catch | _ => pure false
 
 @[implemented_by parserDescrNameHasAtomsUnsafe]
-opaque parserDescrNameHasAtoms (atoms : List String) (p : Name) : TermElabM Bool
+private opaque parserDescrNameHasAtoms (atoms : List String) (p : Name) : TermElabM Bool
 
-def kindHasAtoms (k : Name) (atoms : List String) : TermElabM Bool := do
+private def kindHasAtoms (k : Name) (atoms : List String) : TermElabM Bool := do
   let env ← getEnv
   if let some ci := env.find? k then
     if let some d := ci.value? then
@@ -312,7 +312,7 @@ def kindHasAtoms (k : Name) (atoms : List String) : TermElabM Bool := do
         return true
   return false
 
-def withAtoms (cat : Name) (atoms : List String) : TermElabM (Array Name) := do
+private def withAtoms (cat : Name) (atoms : List String) : TermElabM (Array Name) := do
   let env ← getEnv
   let some catContents := (Lean.Parser.parserExtension.getState env).categories.find? cat
     | return #[]
@@ -323,7 +323,7 @@ def withAtoms (cat : Name) (atoms : List String) : TermElabM (Array Name) := do
       found := found.push k
   return found
 
-def kwImpl (cat : Ident := mkIdent .anonymous) (of : Ident := mkIdent .anonymous)
+private def kwImpl (cat : Ident := mkIdent .anonymous) (of : Ident := mkIdent .anonymous)
     (suggest : Bool)
     (s : StrLit) : TermElabM (Inline ElabInline) := do
   let atoms := s.getString |>.split Char.isWhitespace |>.toStringList

src/Lean/Elab/Import.lean

@@ -10,7 +10,6 @@ public import Lean.Parser.Module
 meta import Lean.Parser.Module
 import Lean.Compiler.ModPkgExt
 public import Lean.DeprecatedModule
-import Init.Data.String.Modify
 
 public section
 
@@ -29,9 +28,7 @@ def HeaderSyntax.isModule (header : HeaderSyntax) : Bool :=
 def HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Array Import :=
   match stx with
   | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) =>
-    let imports := if preludeTk.isNone && includeInit then
-        #[{ module := `Init : Import }, { module := `Init, isMeta := true : Import }]
-      else #[]
+    let imports := if preludeTk.isNone && includeInit then #[{ module := `Init : Import }] else #[]
     imports ++ importsStx.map fun
       | `(Parser.Module.import| $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
         { module := n.getId, importAll := allTk.isSome
@@ -98,43 +95,6 @@ def checkDeprecatedImports
       | none => messages
     | none => messages
 
-private def osForbiddenChars : Array Char :=
-  #['<', '>', '"', '|', '?', '*', '!']
-
-private def osForbiddenNames : Array String :=
-  #["CON", "PRN", "AUX", "NUL",
-    "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
-    "COM¹", "COM²", "COM³",
-    "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9",
-    "LPT¹", "LPT²", "LPT³"]
-
-private def checkComponentPortability (comp : String) : Option String :=
-  if osForbiddenNames.contains comp.toUpper then
-    some s!"'{comp}' is a reserved file name on some operating systems"
-  else if let some c := osForbiddenChars.find? (comp.contains ·) then
-    some s!"contains character '{c}' which is forbidden on some operating systems"
-  else
-    none
-
-def checkModuleNamePortability
-    (mainModule : Name) (inputCtx : Parser.InputContext) (startPos : String.Pos.Raw)
-    (messages : MessageLog) : MessageLog :=
-  go mainModule messages
-where
-  go : Name → MessageLog → MessageLog
-    | .anonymous, messages => messages
-    | .str parent s, messages =>
-      let messages := match checkComponentPortability s with
-        | some reason => messages.add {
-            fileName := inputCtx.fileName
-            pos := inputCtx.fileMap.toPosition startPos
-            severity := .error
-            data := s!"module name '{mainModule}' is not portable: {reason}"
-          }
-        | none => messages
-      go parent messages
-    | .num parent _, messages => go parent messages
-
 def processHeaderCore
     (startPos : String.Pos.Raw) (imports : Array Import) (isModule : Bool)
     (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
@@ -162,7 +122,6 @@ def processHeaderCore
     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
   let env := env.setMainModule mainModule |>.setModulePackage package?
   let messages := checkDeprecatedImports env imports opts inputCtx startPos messages headerStx? origHeaderStx?
-  let messages := checkModuleNamePortability mainModule inputCtx startPos messages
   return (env, messages)
 
 /--

src/Lean/Elab/ParseImportsFast.lean

@@ -233,7 +233,7 @@ def setImportAll : Parser := fun _ s =>
 
 def main : Parser :=
   keywordCore "module" (setIsModule false) (setIsModule true) >>
-  keywordCore "prelude" (fun _ s => (s.pushImport `Init).pushImport { module := `Init, isMeta := true }) skip >>
+  keywordCore "prelude" (fun _ s => s.pushImport `Init) skip >>
   manyImports (atomic (keywordCore "public" skip setExported >>
     keywordCore "meta" skip setMeta >>
     keyword "import") >>

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -55,7 +55,7 @@ def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withC
     -- Else use delta reduction
     deltaLHS mvarId
 
-partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do
+private partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do
   withTraceNode `Elab.definition.eqns (fun _ => return m!"proving:{indentExpr type}") do
   withNewMCtxDepth do
     let main ← mkFreshExprSyntheticOpaqueMVar type
@@ -102,7 +102,7 @@ partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do
         else
           throwError "failed to generate equational theorem for `{.ofConstName declName}`\n{MessageData.ofGoal mvarId}"
 
-def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
+private def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
   forallTelescope type fun _ type => do
     if let some (_, lhs, _) ← matchEq? type then
       dependsOn lhs fvarId

src/Lean/Elab/Quotation/Precheck.lean

@@ -113,7 +113,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
     if (← read).quotLCtx.contains val then
       return
     let rs ← try resolveName stx val [] [] catch _ => pure []
-    for (e, _, _) in rs do
+    for (e, _) in rs do
       match e with
       | Expr.fvar _      .. =>
         if quotPrecheck.allowSectionVars.get (← getOptions) && (← isSectionVariable e) then

src/Lean/Elab/StructInst.lean

@@ -150,8 +150,6 @@ structure SourcesView where
   explicit : Array ExplicitSourceView
   /-- The syntax for a trailing `..`. This is "ellipsis mode" for missing fields, similar to ellipsis mode for applications. -/
   implicit : Option Syntax
-  /-- Use `Inhabited` instances inherited from parent structures, and use `default` instances for missing fields. -/
-  useInhabited : Bool
   deriving Inhabited
 
 /--
@@ -181,7 +179,7 @@ private def getStructSources (structStx : Syntax) : TermElabM SourcesView :=
         let structName ← getStructureName srcType
         return { stx, fvar := src, structName }
     let implicit := if implicitSource[0].isNone then none else implicitSource
-    return { explicit, implicit, useInhabited := false }
+    return { explicit, implicit }
 
 /--
 We say a structure instance notation is a "modifyOp" if it contains only a single array update.
@@ -581,9 +579,6 @@ private structure StructInstContext where
   /-- If true, then try using default values or autoParams for missing fields.
   (Considered after `useParentInstanceFields`.) -/
   useDefaults : Bool
-  /-- If true, then tries `Inhabited` instances as an alternative to parent instances,
-  and when default values are missing. -/
-  useInhabited : Bool
   /-- If true, then missing fields after default value synthesis remain as metavariables rather than yielding an error.
   Only applies if `useDefaults` is true. -/
   unsynthesizedAsMVars : Bool
@@ -740,27 +735,14 @@ The arguments for the `_default` auxiliary function are provided by `fieldMap`.
 After default values are resolved, then the one that is added to the environment
 as an `_inherited_default` auxiliary function is normalized; we don't do those normalizations here.
 -/
-private def getFieldDefaultValue? (fieldName : Name) : StructInstM (Option (NameSet × Expr)) := do
+private partial def getFieldDefaultValue? (fieldName : Name) : StructInstM (NameSet × Option Expr) := do
   let some defFn := getEffectiveDefaultFnForField? (← getEnv) (← read).structName fieldName
-    | return none
+    | return ({}, none)
   let fieldMap := (← get).fieldMap
   let some (fields, val) ← instantiateStructDefaultValueFn? defFn (← read).levels (← read).params (pure ∘ fieldMap.find?)
     | logError m!"default value for field `{fieldName}` of structure `{.ofConstName (← read).structName}` could not be instantiated, ignoring"
-      return none
-  return some (fields, val)
-
-/--
-If `useInhabited` is enabled, tries synthesizing an `Inhabited` instance for the field.
--/
-private def getFieldDefaultValueUsingInhabited (fieldType : Expr) : StructInstM (Option (NameSet × Expr)) := do
-  if (← read).useInhabited then
-    try
-      let val ← mkDefault fieldType
-      return some ({}, val)
-    catch _ =>
-      return none
-  else
-    return none
+      return ({}, none)
+  return (fields, val)
 
 /--
 Auxiliary type for `synthDefaultFields`
@@ -769,16 +751,8 @@ private structure PendingField where
   fieldName : Name
   fieldType : Expr
   required : Bool
-  /-- If present, field dependencies and the default value. -/
-  val? : Option (NameSet × Expr)
-
-private def PendingField.isReady (pendingField : PendingField) (hasDep : Name → Bool) : Bool :=
-  pendingField.val?.any fun (deps, _) => deps.all hasDep
-
-private def PendingField.val! (pendingField : PendingField) : Expr :=
-  match pendingField.val? with
-  | some (_, val) => val
-  | none          => panic! "PendingField has no value"
+  deps : NameSet
+  val? : Option Expr
 
 private def registerFieldMVarError (e : Expr) (ref : Syntax) (fieldName : Name) : StructInstM Unit :=
   registerCustomErrorIfMVar e ref m!"Cannot synthesize placeholder for field `{fieldName}`"
@@ -812,15 +786,12 @@ private def synthOptParamFields : StructInstM Unit := do
   -- Process default values for pending optParam fields.
   let mut pendingFields : Array PendingField ← optParamFields.filterMapM fun (fieldName, fieldType, required) => do
     if required || (← isFieldNotSolved? fieldName).isSome then
-      let val? ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure none
-      let val? ← pure val? <||> if (← read).useInhabited then getFieldDefaultValueUsingInhabited fieldType else pure none
-      trace[Elab.struct]
-        if let some (deps, val) := val? then
-          m!"default value for {fieldName}:{inlineExpr val}" ++
-          if deps.isEmpty then m!"" else m!"(depends on fields {deps.toArray})"
-        else
-          m!"no default value for {fieldName}"
-      pure <| some { fieldName, fieldType, required, val? }
+      let (deps, val?) ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure ({}, none)
+      if let some val := val? then
+        trace[Elab.struct] "default value for {fieldName}:{indentExpr val}"
+      else
+        trace[Elab.struct] "no default value for {fieldName}"
+      pure <| some { fieldName, fieldType, required, deps, val? }
     else
       pure none
   -- We then iteratively look for pending fields that do not depend on unsolved-for fields.
@@ -828,11 +799,12 @@ private def synthOptParamFields : StructInstM Unit := do
   -- so we need to keep trying until no more progress is made.
   let mut pendingSet : NameSet := pendingFields.foldl (init := {}) fun set pending => set.insert pending.fieldName
   while !pendingSet.isEmpty do
-    let selectedFields := pendingFields.filter (·.isReady (!pendingSet.contains ·))
+    let selectedFields := pendingFields.filter fun pendingField =>
+      pendingField.val?.isSome && pendingField.deps.all (fun dep => !pendingSet.contains dep)
     let mut toRemove : Array Name := #[]
     let mut assignErrors : Array MessageData := #[]
     for selected in selectedFields do
-      let selectedVal := selected.val!
+      let some selectedVal := selected.val? | unreachable!
       if let some mvarId ← isFieldNotSolved? selected.fieldName then
         let fieldType := selected.fieldType
         let selectedType ← inferType selectedVal
@@ -1112,7 +1084,6 @@ private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : B
         addStructFieldAux fieldName mvar
         return ← loop
   -- Default case: natural metavariable, register it for optParams
-  let fieldType := fieldType.consumeTypeAnnotations
   discard <| addStructFieldMVar fieldName fieldType
   modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
   loop
@@ -1140,44 +1111,29 @@ private partial def loop : StructInstM Expr := withViewRef do
 For each parent class, see if it can be used to synthesize the fields that haven't been provided.
 -/
 private partial def addParentInstanceFields : StructInstM Unit := do
+  let env ← getEnv
   let structName := (← read).structName
-  let fieldNames := getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false)
+  let fieldNames := getStructureFieldsFlattened env structName (includeSubobjectFields := false)
   let fieldViews := (← read).fieldViews
   if fieldNames.all fieldViews.contains then
     -- Every field is accounted for already
     return
 
-  -- We look at parents in resolution order
+  -- We look at class parents in resolution order
   let parents ← getAllParentStructures structName
-  let env ← getEnv
-  let parentsToVisit := if (← read).useInhabited then parents else parents.filter (isClass env)
-  if parentsToVisit.isEmpty then return
+  let classParents := parents.filter (isClass env)
+  if classParents.isEmpty then return
 
   let allowedFields := fieldNames.filter (!fieldViews.contains ·)
   let mut remainingFields := allowedFields
 
   -- Worklist of parent/fields pairs. If fields is empty, then it will be computed later.
-  let mut worklist : List (Name × Array Name) := parentsToVisit |>.map (·, #[]) |>.toList
+  let mut worklist : List (Name × Array Name) := classParents |>.map (·, #[]) |>.toList
   let mut deferred : List (Name × Array Name) := []
 
-  let trySynthParent (parentName : Name) (parentTy : Expr) : StructInstM (LOption Expr) := do
-    if isClass (← getEnv) parentName then
-      match ← trySynthInstance parentTy with
-      | .none => pure ()
-      | r     => return r
-    if (← read).useInhabited then
-      let u ← getLevel parentTy
-      let cls := Expr.app (Expr.const ``Inhabited [u]) parentTy
-      match ← trySynthInstance cls with
-      | .none      => pure ()
-      | .undef     => return .undef
-      | .some inst => return .some <| mkApp2 (Expr.const ``Inhabited.default [u]) parentTy inst
-    return .none
-
   while !worklist.isEmpty do
     let (parentName, parentFields) :: worklist' := worklist | unreachable!
     worklist := worklist'
-    let env ← getEnv
     let parentFields := if parentFields.isEmpty then getStructureFieldsFlattened env parentName (includeSubobjectFields := false) else parentFields
     -- We only try synthesizing if the parent contains one of the remaining fields
     -- and if every parent field is an allowed field.
@@ -1189,7 +1145,7 @@ private partial def addParentInstanceFields : StructInstM Unit := do
         trace[Elab.struct] "could not calculate type for parent `{.ofConstName parentName}`"
         deferred := (parentName, parentFields) :: deferred
       | some (parentTy, _) =>
-        match ← trySynthParent parentName parentTy with
+        match ← trySynthInstance parentTy with
         | .none => trace[Elab.struct] "failed to synthesize instance for parent {parentTy}"
         | .undef =>
           trace[Elab.struct] "instance synthesis stuck for parent {parentTy}"
@@ -1243,19 +1199,17 @@ private def elabStructInstView (s : StructInstView) (structName : Name) (structT
   let fields ← addSourceFields structName s.sources.explicit fields
   trace[Elab.struct] "expanded fields:\n{MessageData.joinSep (fields.toList.map (fun (_, field) => m!"- {MessageData.nestD (toMessageData field)}")) "\n"}"
   let ellipsis := s.sources.implicit.isSome
-  let useInhabited := s.sources.useInhabited
   let (val, _) ← main
     |>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn
              -- See the note in `ElabAppArgs.processExplicitArg`
              -- For structure instances though, there's a sense in which app-style ellipsis mode is always enabled,
              -- so we do not specifically check for it to disable defaults.
              -- An effect of this is that if a user forgets `..` they'll be reminded with a "Fields missing" error.
-             useDefaults := !(← readThe Term.Context).inPattern || useInhabited
+             useDefaults := !(← readThe Term.Context).inPattern
              -- Similarly, for patterns we disable using parent instances to fill in fields
-             useParentInstanceFields := !(← readThe Term.Context).inPattern || useInhabited
+             useParentInstanceFields := !(← readThe Term.Context).inPattern
              -- In ellipsis mode, unsynthesized missing fields become metavariables, rather than being an error
              unsynthesizedAsMVars := ellipsis
-             useInhabited := useInhabited
      }
     |>.run { type := ctorFnType }
   return val
@@ -1379,15 +1333,6 @@ where
       trace[Elab.struct] "result:{indentExpr r}"
       return r
 
-@[builtin_term_elab structInstDefault] def elabStructInstDefault : TermElab := fun stx expectedType? => do
-  let sourcesView : SourcesView := { explicit := #[], implicit := none, useInhabited := true }
-  let (structName, structType?) ← getStructName expectedType? sourcesView
-  withTraceNode `Elab.struct (fun _ => return m!"elaborating default value for `{structName}`") do
-    let struct : StructInstView := { ref := stx, fields := #[], sources := sourcesView }
-    let r ← withSynthesize (postpone := .yes) <| elabStructInstView struct structName structType?
-    trace[Elab.struct] "result:{indentExpr r}"
-    return r
-
 builtin_initialize
   registerTraceClass `Elab.struct
   registerTraceClass `Elab.struct.modifyOp

src/Lean/Elab/Term/TermElabM.lean

@@ -232,10 +232,7 @@ structure TacticFinishedSnapshot extends Language.Snapshot where
   state? : Option SavedState
   /-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation. -/
   moreSnaps : Array (SnapshotTask SnapshotTree)
-
-instance : Inhabited TacticFinishedSnapshot where
-  default := { toSnapshot := default, state? := default, moreSnaps := default }
-
+deriving Inhabited
 instance : ToSnapshotTree TacticFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, s.moreSnaps⟩
 
@@ -249,10 +246,7 @@ structure TacticParsedSnapshot extends Language.Snapshot where
   finished : SnapshotTask TacticFinishedSnapshot
   /-- Tasks for subsequent, potentially parallel, tactic steps. -/
   next     : Array (SnapshotTask TacticParsedSnapshot) := #[]
-
-instance : Inhabited TacticParsedSnapshot where
-  default := { toSnapshot := default, stx := default, finished := default }
-
+deriving Inhabited
 partial instance : ToSnapshotTree TacticParsedSnapshot where
   toSnapshotTree := go where
     go := fun s => ⟨s.toSnapshot,
@@ -633,13 +627,13 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl
   `[LVal.fieldName "foo", LVal.fieldIdx 1]`.
 -/
 inductive LVal where
-  | fieldIdx  (ref : Syntax) (i : Nat) (levels : List Level)
+  | fieldIdx  (ref : Syntax) (i : Nat)
   /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierarchical/composite name.
   `ref` is the syntax object representing the field. `fullRef` includes the LHS. -/
-  | fieldName (ref : Syntax) (name : String) (levels : List Level) (suffix? : Option Name) (fullRef : Syntax)
+  | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (fullRef : Syntax)
 
 def LVal.getRef : LVal → Syntax
-  | .fieldIdx ref ..   => ref
+  | .fieldIdx ref _    => ref
   | .fieldName ref ..  => ref
 
 def LVal.isFieldName : LVal → Bool
@@ -648,11 +642,8 @@ def LVal.isFieldName : LVal → Bool
 
 instance : ToString LVal where
   toString
-    | .fieldIdx _ i levels ..  => toString i ++ levelsToString levels
-    | .fieldName _ n levels .. => n ++ levelsToString levels
-where
-  levelsToString levels :=
-    if levels.isEmpty then "" else ".{" ++ String.intercalate "," (levels.map toString) ++ "}"
+    | .fieldIdx _ i     => toString i
+    | .fieldName _ n .. => n
 
 /-- Return the name of the declaration being elaborated if available. -/
 def getDeclName? : TermElabM (Option Name) := return (← read).declName?
@@ -2120,10 +2111,8 @@ def checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit := do
 @[inline] def withoutCheckDeprecated [MonadWithReaderOf Context m] : m α → m α :=
   withTheReader Context (fun ctx => { ctx with checkDeprecated := false })
 
-private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String × List Level)) := do
+private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do
-    -- levels apply to the last projection, not the constant
-    let (constLevels, projLevels) := if projs.isEmpty then (explicitLevels, []) else ([], explicitLevels)
     -- TODO: better support for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail.
     /-
     We disable `checkDeprecated` here because there may be many overloaded symbols.
@@ -2132,38 +2121,25 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     At `elabAppFnId`, we perform the check when converting the list returned by `resolveName'` into a list of
     `TermElabResult`s.
     -/
-    let const ← withoutCheckDeprecated <| mkConst declName constLevels
-    return (const, projs, projLevels) :: result
+    let const ← withoutCheckDeprecated <| mkConst declName explicitLevels
+    return (const, projs) :: result
 
 def throwInvalidExplicitUniversesForLocal {α} (e : Expr) : TermElabM α :=
   throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
 
-/--
-  Gives all resolutions of the name `n`.
-
-- `explicitLevels` provides a prefix of level parameters to the constant. For resolutions with a projection
-  component, the levels are not used, since they must apply to the last projection, not the constant.
-  In that case, the third component of the tuple is `explicitLevels`.
--/
-def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String × List Level)) := do
+def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
   addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
-  let processLocal (e : Expr) (projs : List String) := do
-    if projs.isEmpty then
-      if explicitLevels.isEmpty then
-        return [(e, [], [])]
-      else
-        throwInvalidExplicitUniversesForLocal e
-    else
-      return [(e, projs, explicitLevels)]
   if let some (e, projs) ← resolveLocalName n then
-    return ← processLocal e projs
+    unless explicitLevels.isEmpty do
+      throwInvalidExplicitUniversesForLocal e
+    return [(e, projs)]
   let preresolved := preresolved.filterMap fun
     | .decl n projs => some (n, projs)
     | _             => none
   -- check for section variable capture by a quotation
   let ctx ← read
   if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
-    return ← processLocal e projs  -- section variables should shadow global decls
+    return [(e, projs)]  -- section variables should shadow global decls
   if preresolved.isEmpty then
     mkConsts (← realizeGlobalName n) explicitLevels
   else
@@ -2172,17 +2148,14 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
 /--
   Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`.
   Example: Assume resolveName `v.head.bla.boo` produces `(v.head, ["bla", "boo"])`, then this method produces
-  `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`.
-
-  See the comment there about `explicitLevels` and the meaning of the `List Level` component of the returned tuple.
--/
-def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax × List Level)) := do
+  `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/
+def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax)) := do
   let .ident _ _ n preresolved := ident
     | throwError "identifier expected"
   let r ← resolveName ident n preresolved explicitLevels expectedType?
-  let rc ← r.mapM fun (c, fields, levels) => do
+  let rc ← r.mapM fun (c, fields) => do
     let ids := ident.identComponents (nFields? := fields.length)
-    return (c, ids.head!, ids.tail!, levels)
+    return (c, ids.head!, ids.tail!)
   return (n, rc)
 
 
@@ -2190,7 +2163,7 @@ def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (
   match stx with
   | .ident _ _ val preresolved =>
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
-    let rs := rs.filter fun ⟨_, projs, _⟩ => projs.isEmpty
+    let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f
     match fs with
     | []  => return none

src/Lean/Environment.lean

@@ -616,13 +616,7 @@ structure Environment where
   /--
   Indicates whether the environment is being used in an exported context, i.e. whether it should
   provide access to only the data to be imported by other modules participating in the module
-  system. Apart from controlling access, some operations such as `mkAuxDeclName` may also change
-  their output based on this flag.
-
-  By default, `isExporting` is set to false when command elaborators are invoked such that they have
-  access to the full local environment. Use `with(out)Exporting` to modify based on context. For
-  example, `elabDeclaration` sets it based on `(← getScope).isPublic` on the top level, then
-  `elabMutualDef` may switch from public to private when e.g. entering the proof of a theorem.
+  system.
   -/
   isExporting : Bool := false
 deriving Nonempty

src/Lean/ErrorExplanation.lean

@@ -73,19 +73,19 @@ def hasErrorExplanation [Monad m] [MonadEnv m] (name : Name) : m Bool :=
   return errorExplanationExt.getState (← getEnv) |>.contains name
 
 /-- Returns all error explanations with their names, sorted by name. -/
-def getErrorExplanations [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do
+public def getErrorExplanations [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do
   return errorExplanationExt.getState (← getEnv)
     |>.toArray
     |>.qsort fun e e' => e.1.toString < e'.1.toString
 
 @[deprecated getErrorExplanations (since := "2026-12-20")]
-def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation) :=
+public def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation) :=
   errorExplanationExt.getState env
     |>.toArray
     |>.qsort fun e e' => e.1.toString < e'.1.toString
 
 @[deprecated getErrorExplanations (since := "2026-12-20")]
-def getErrorExplanationsSorted [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do
+public def getErrorExplanationsSorted [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do
   getErrorExplanations
 
 end Lean

src/Lean/Language/Basic.lean

@@ -67,9 +67,7 @@ structure Snapshot where
   `diagnostics`) occurred that prevents processing of the remainder of the file.
   -/
   isFatal := false
-
-instance : Inhabited Snapshot where
-  default := { desc := "", diagnostics := default }
+deriving Inhabited
 
 /-- Range that is marked as being processed by the server while a task is running. -/
 inductive SnapshotTask.ReportingRange where
@@ -238,10 +236,7 @@ partial def SnapshotTask.cancelRec [ToSnapshotTree α] (t : SnapshotTask α) : B
 
 /-- Snapshot type without child nodes. -/
 structure SnapshotLeaf extends Snapshot
-deriving TypeName
-
-instance : Inhabited SnapshotLeaf where
-  default := { toSnapshot := default }
+deriving Inhabited, TypeName
 
 instance : ToSnapshotTree SnapshotLeaf where
   toSnapshotTree s := SnapshotTree.mk s.toSnapshot #[]

src/Lean/Linter.lean

@@ -19,4 +19,3 @@ public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
 public import Lean.Linter.Coe
 public import Lean.Linter.GlobalAttributeIn
-public import Lean.Linter.EnvLinter

src/Lean/Linter/EnvLinter.lean

@@ -1,10 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
--/
-module
-
-prelude
-public import Lean.Linter.EnvLinter.Basic
-public import Lean.Linter.EnvLinter.Frontend

src/Lean/Linter/EnvLinter/Basic.lean

@@ -1,163 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
-
-Copyright (c) 2020 Floris van Doorn. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
--/
-module
-
-prelude
-public import Lean.Structure
-public import Lean.Elab.InfoTree.Main
-import Lean.ExtraModUses
-
-public section
-
-open Lean Meta
-
-namespace Lean.Linter.EnvLinter
-
-/-!
-# Basic environment linter types and attributes
-
-This file defines the basic types and attributes used by the environment
-linting framework. An environment linter consists of a function
-`(declaration : Name) → MetaM (Option MessageData)`, this function together with some
-metadata is stored in the `EnvLinter` structure. We define two attributes:
-
- * `@[builtin_env_linter]` applies to a declaration of type `EnvLinter`
-   and adds it to the default linter set.
-
- * `@[builtin_nolint linterName]` omits the tagged declaration from being checked by
-   the linter with name `linterName`.
--/
-
-/--
-Returns true if `decl` is an automatically generated declaration.
-
-Also returns true if `decl` is an internal name or created during macro
-expansion.
--/
-def isAutoDecl (decl : Name) : CoreM Bool := do
-  if decl.hasMacroScopes then return true
-  if decl.isInternal then return true
-  let env ← getEnv
-  if isReservedName env decl then return true
-  if let Name.str n s := decl then
-    if (← isAutoDecl n) then return true
-    if s.startsWith "proof_"
-        || s.startsWith "match_"
-        || s.startsWith "unsafe_"
-        || s.startsWith "grind_"
-    then return true
-    if env.isConstructor n && s ∈ ["injEq", "inj", "sizeOf_spec", "elim", "noConfusion"] then
-      return true
-    if let ConstantInfo.inductInfo _ := env.find? n then
-      if s.startsWith "brecOn_" || s.startsWith "below_" then return true
-      if s ∈ [casesOnSuffix, recOnSuffix, brecOnSuffix, belowSuffix,
-          "ndrec", "ndrecOn", "noConfusionType", "noConfusion", "ofNat", "toCtorIdx", "ctorIdx",
-          "ctorElim", "ctorElimType"] then
-        return true
-      if let some _ := isSubobjectField? env n (.mkSimple s) then
-        return true
-    -- Coinductive/inductive lattice-theoretic predicates:
-    if let ConstantInfo.inductInfo _ := env.find? (Name.str n "_functor") then
-      if s == "functor_unfold" || s == casesOnSuffix || s == "mutual" then return true
-      if env.isConstructor (Name.str (Name.str n "_functor") s) then return true
-  pure false
-
-/-- An environment linting test for the `lake builtin-lint` command. -/
-structure EnvLinter where
-  /-- `test` defines a test to perform on every declaration. It should never fail. Returning `none`
-  signifies a passing test. Returning `some msg` reports a failing test with error `msg`. -/
-  test : Name → MetaM (Option MessageData)
-  /-- `noErrorsFound` is the message printed when all tests are negative -/
-  noErrorsFound : MessageData
-  /-- `errorsFound` is printed when at least one test is positive -/
-  errorsFound : MessageData
-  /-- If `isDefault` is false, this linter is only run when `--clippy` is passed. -/
-  isDefault := true
-
-/-- A `NamedEnvLinter` is an environment linter associated to a particular declaration. -/
-structure NamedEnvLinter extends EnvLinter where
-  /-- The name of the named linter. This is just the declaration name without the namespace. -/
-  name : Name
-  /-- The linter declaration name -/
-  declName : Name
-
-/-- Gets an environment linter by declaration name. -/
-def getEnvLinter (name declName : Name) : CoreM NamedEnvLinter := unsafe
-  return { ← evalConstCheck EnvLinter ``EnvLinter declName with name, declName }
-
-/-- Defines the `envLinterExt` extension for adding an environment linter to the default set. -/
-builtin_initialize envLinterExt :
-    SimplePersistentEnvExtension (Name × Bool) (NameMap (Name × Bool)) ←
-  let addEntryFn := fun m (n, b) => m.insert (n.updatePrefix .anonymous) (n, b)
-  registerSimplePersistentEnvExtension {
-    addImportedFn := fun nss =>
-      nss.foldl (init := {}) fun m ns => ns.foldl (init := m) addEntryFn
-    addEntryFn
-  }
-
-/--
-Defines the `@[builtin_env_linter]` attribute for adding a linter to the default set.
-The form `@[builtin_env_linter clippy]` will not add the linter to the default set,
-but it can be selected by `lake builtin-lint --clippy`.
-
-Linters are named using their declaration names, without the namespace. These must be distinct.
--/
-syntax (name := builtin_env_linter) "builtin_env_linter" &" clippy"? : attr
-
-builtin_initialize registerBuiltinAttribute {
-  name := `builtin_env_linter
-  descr := "Use this declaration as a linting test in `lake builtin-lint`"
-  add   := fun decl stx kind => do
-    let dflt := stx[1].isNone
-    unless kind == .global do throwError "invalid attribute `builtin_env_linter`, must be global"
-    let shortName := decl.updatePrefix .anonymous
-    if let some (declName, _) := (envLinterExt.getState (← getEnv)).find? shortName then
-      Elab.addConstInfo stx declName
-      throwError
-        "invalid attribute `builtin_env_linter`, linter `{shortName}` has already been declared"
-    let isPublic := !isPrivateName decl; let isMeta := isMarkedMeta (← getEnv) decl
-    unless isPublic && isMeta do
-      throwError "invalid attribute `builtin_env_linter`, \
-        declaration `{.ofConstName decl}` must be marked as `public` and `meta`\
-        {if isPublic then " but is only marked `public`" else ""}\
-        {if isMeta then " but is only marked `meta`" else ""}"
-    let constInfo ← getConstInfo decl
-    unless ← (isDefEq constInfo.type (mkConst ``EnvLinter)).run' do
-      throwError "`{.ofConstName decl}` must have type `{.ofConstName ``EnvLinter}`, got \
-        `{constInfo.type}`"
-    modifyEnv fun env => envLinterExt.addEntry env (decl, dflt)
-}
-
-/-- `@[builtin_nolint linterName]` omits the tagged declaration from being checked by
-the linter with name `linterName`. -/
-syntax (name := builtin_nolint) "builtin_nolint" (ppSpace ident)+ : attr
-
-/-- Defines the user attribute `builtin_nolint` for skipping environment linters. -/
-builtin_initialize builtinNolintAttr : ParametricAttribute (Array Name) ←
-  registerParametricAttribute {
-    name := `builtin_nolint
-    descr := "Do not report this declaration in any of the tests of `lake builtin-lint`"
-    getParam := fun _ => fun
-      | `(attr| builtin_nolint $[$ids]*) => ids.mapM fun id => withRef id <| do
-        let shortName := id.getId.eraseMacroScopes
-        let some (declName, _) := (envLinterExt.getState (← getEnv)).find? shortName
-          | throwError "linter '{shortName}' not found"
-        Elab.addConstInfo id declName
-        recordExtraModUseFromDecl (isMeta := false) declName
-        pure shortName
-      | _ => Elab.throwUnsupportedSyntax
-  }
-
-/-- Returns true if `decl` should be checked
-using `linter`, i.e., if there is no `builtin_nolint` attribute. -/
-def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool :=
-  return !((builtinNolintAttr.getParam? (← getEnv) decl).getD #[]).contains linter
-
-end Lean.Linter.EnvLinter

src/Lean/Linter/EnvLinter/Frontend.lean

@@ -1,180 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
-
-Copyright (c) 2020 Floris van Doorn. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
--/
-module
-
-prelude
-public import Lean.Linter.EnvLinter.Basic
-import Lean.DeclarationRange
-import Lean.Util.Path
-import Lean.CoreM
-import Lean.Elab.Command
-
-public section
-
-open Lean Meta
-
-namespace Lean.Linter.EnvLinter
-
-/-- Verbosity for the linter output. -/
-inductive LintVerbosity
-  /-- `low`: only print failing checks, print nothing on success. -/
-  | low
-  /-- `medium`: only print failing checks, print confirmation on success. -/
-  | medium
-  /-- `high`: print output of every check. -/
-  | high
-  deriving Inhabited, DecidableEq, Repr
-
-/-- `getChecks clippy runOnly` produces a list of linters.
-`runOnly` is an optional list of names that should resolve to declarations with type
-`NamedEnvLinter`. If populated, only these linters are run (regardless of the default
-configuration). Otherwise, it uses all enabled linters in the environment tagged with
-`@[builtin_env_linter]`. If `clippy` is false, it only uses linters with `isDefault = true`. -/
-def getChecks (clippy : Bool) (runOnly : Option (List Name)) :
-    CoreM (Array NamedEnvLinter) := do
-  let mut result := #[]
-  for (name, declName, isDefault) in envLinterExt.getState (← getEnv) do
-    let shouldRun := match runOnly with
-      | some only => only.contains name
-      | none => clippy || isDefault
-    if shouldRun then
-      let linter ← getEnvLinter name declName
-      result := result.binInsert (·.name.lt ·.name) linter
-  pure result
-
-
-/--
-Runs all the specified linters on all the specified declarations in parallel,
-producing a list of results.
--/
-def lintCore (decls : Array Name) (linters : Array NamedEnvLinter) :
-    CoreM (Array (NamedEnvLinter × Std.HashMap Name MessageData)) := do
-  let tasks : Array (NamedEnvLinter × Array (Name × Task (Except Exception <| Option MessageData))) ←
-    linters.mapM fun linter => do
-      let decls ← decls.filterM (shouldBeLinted linter.name)
-      (linter, ·) <$> decls.mapM fun decl => (decl, ·) <$> do
-        let act : MetaM (Option MessageData) := do
-          linter.test decl
-        EIO.asTask <| (← Core.wrapAsync (fun _ =>
-          act |>.run' Elab.Command.mkMetaContext
-        ) (cancelTk? := none)) ()
-
-  let result ← tasks.mapM fun (linter, decls) => do
-    let mut msgs : Std.HashMap Name MessageData := {}
-    for (declName, msgTask) in decls do
-      let msg? ← match msgTask.get with
-      | Except.ok msg? => pure msg?
-      | Except.error err => pure m!"LINTER FAILED:\n{err.toMessageData}"
-      if let .some msg := msg? then
-        msgs := msgs.insert declName msg
-    pure (linter, msgs)
-  return result
-
-/-- Sorts a map with declaration keys as names by line number. -/
-def sortResults (results : Std.HashMap Name α) : CoreM <| Array (Name × α) := do
-  let mut key : Std.HashMap Name Nat := {}
-  for (n, _) in results.toArray do
-    if let some range ← findDeclarationRanges? n then
-      key := key.insert n <| range.range.pos.line
-  pure $ results.toArray.qsort fun (a, _) (b, _) => key.getD a 0 < key.getD b 0
-
-/-- Formats a linter warning as `#check` command with comment. -/
-def printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Bool := false)
-  (filePath : System.FilePath := default) : CoreM MessageData := do
-  if useErrorFormat then
-    if let some range ← findDeclarationRanges? declName then
-      let msg ← addMessageContextPartial
-        m!"{filePath}:{range.range.pos.line}:{range.range.pos.column + 1}: error: {
-          ← mkConstWithLevelParams declName} {warning}"
-      return msg
-  addMessageContextPartial m!"#check {← mkConstWithLevelParams declName} /- {warning} -/"
-
-/-- Formats a map of linter warnings using `printWarning`, sorted by line number. -/
-def printWarnings (results : Std.HashMap Name MessageData) (filePath : System.FilePath := default)
-    (useErrorFormat : Bool := false) : CoreM MessageData := do
-  (MessageData.joinSep ·.toList Format.line) <$>
-    (← sortResults results).mapM fun (declName, warning) =>
-      printWarning declName warning (useErrorFormat := useErrorFormat) (filePath := filePath)
-
-/--
-Formats a map of linter warnings grouped by filename with `-- filename` comments.
--/
-def groupedByFilename (results : Std.HashMap Name MessageData) (useErrorFormat : Bool := false) :
-    CoreM MessageData := do
-  let sp ← if useErrorFormat then getSrcSearchPath else pure {}
-  let grouped : Std.HashMap Name (System.FilePath × Std.HashMap Name MessageData) ←
-    results.foldM (init := {}) fun grouped declName msg => do
-      let mod ← findModuleOf? declName
-      let mod := mod.getD (← getEnv).mainModule
-      grouped.insert mod <$>
-        match grouped[mod]? with
-        | some (fp, msgs) => pure (fp, msgs.insert declName msg)
-        | none => do
-          let fp ← if useErrorFormat then
-            pure <| (← sp.findWithExt "lean" mod).getD (modToFilePath "." mod "lean")
-          else pure default
-          pure (fp, .insert {} declName msg)
-  let grouped' := grouped.toArray.qsort fun (a, _) (b, _) => toString a < toString b
-  (MessageData.joinSep · (Format.line ++ Format.line)) <$>
-    grouped'.toList.mapM fun (mod, fp, msgs) => do
-      pure m!"-- {mod}\n{← printWarnings msgs (filePath := fp) (useErrorFormat := useErrorFormat)}"
-
-/--
-Formats the linter results as Lean code with comments and `#check` commands.
--/
-def formatLinterResults
-    (results : Array (NamedEnvLinter × Std.HashMap Name MessageData))
-    (decls : Array Name)
-    (groupByFilename : Bool)
-    (whereDesc : String) (runClippyLinters : Bool)
-    (verbose : LintVerbosity) (numLinters : Nat) (useErrorFormat : Bool := false) :
-    CoreM MessageData := do
-  let formattedResults ← results.filterMapM fun (linter, results) => do
-    if !results.isEmpty then
-      let warnings ←
-        if groupByFilename || useErrorFormat then
-          groupedByFilename results (useErrorFormat := useErrorFormat)
-        else
-          printWarnings results
-      pure $ some m!"/- The `{linter.name}` linter reports:\n{linter.errorsFound} -/\n{warnings}\n"
-    else if verbose = LintVerbosity.high then
-      pure $ some m!"/- OK: {linter.noErrorsFound} -/"
-    else
-      pure none
-  let mut s := MessageData.joinSep formattedResults.toList Format.line
-  let numAutoDecls := (← decls.filterM isAutoDecl).size
-  let failed := results.map (·.2.size) |>.foldl (·+·) 0
-  unless verbose matches LintVerbosity.low do
-    s := m!"-- Found {failed} error{if failed == 1 then "" else "s"
-      } in {decls.size - numAutoDecls} declarations (plus {
-      numAutoDecls} automatically generated ones) {whereDesc
-      } with {numLinters} linters\n\n{s}"
-  unless runClippyLinters do s := m!"{s}-- (non-clippy linters skipped)\n"
-  pure s
-
-/-- Get the list of declarations in the current module. -/
-def getDeclsInCurrModule : CoreM (Array Name) := do
-  pure $ (← getEnv).constants.map₂.foldl (init := #[]) fun r k _ => r.push k
-
-/-- Get the list of all declarations in the environment. -/
-def getAllDecls : CoreM (Array Name) := do
-  pure $ (← getEnv).constants.map₁.fold (init := ← getDeclsInCurrModule) fun r k _ => r.push k
-
-/-- Get the list of all declarations in the specified package. -/
-def getDeclsInPackage (pkg : Name) : CoreM (Array Name) := do
-  let env ← getEnv
-  let mut decls ← getDeclsInCurrModule
-  let modules := env.header.moduleNames.map (pkg.isPrefixOf ·)
-  return env.constants.map₁.fold (init := decls) fun decls declName _ =>
-    if modules[env.const2ModIdx[declName]?.get!]! then
-      decls.push declName
-    else decls
-
-end Lean.Linter.EnvLinter

src/Lean/Meta/Constructions/BRecOn.lean

@@ -30,7 +30,7 @@ of type
 α → List α → Sort (max 1 u_1) → Sort (max 1 u_1)
 ```
 -/
-def buildBelowMinorPremise (rlvl : Level) (motives : Array Expr) (minorType : Expr) : MetaM Expr :=
+private def buildBelowMinorPremise (rlvl : Level) (motives : Array Expr) (minorType : Expr) : MetaM Expr :=
   forallTelescope minorType fun minor_args _ => do go #[] minor_args.toList
 where
   go (prods : Array Expr) : List Expr → MetaM Expr
@@ -56,7 +56,7 @@ For example for the `List` type, it constructs,
 fun {a} {motive} t => List.rec PUnit (fun a_1 a a_ih => motive a ×' a_ih) t
 ```
 -/
-def mkBelowFromRec (recName : Name) (nParams : Nat)
+private def mkBelowFromRec (recName : Name) (nParams : Nat)
   (belowName : Name) : MetaM Unit := do
   -- The construction follows the type of `ind.rec`
   let .recInfo recVal ← getConstInfo recName
@@ -146,7 +146,7 @@ of type
   PProd (motive (head :: tail)) (PProd (PProd (motive tail) (List.below tail)) PUnit)
 ```
 -/
-def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
+private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
     (belows : Array Expr) (fs : Array Expr) (minorType : Expr) : MetaM Expr :=
   forallTelescope minorType fun minor_args minor_type => do
     let rec go (prods : Array Expr) : List Expr → MetaM Expr
@@ -188,7 +188,7 @@ protected theorem List.brecOn.eq.{u} : ∀ {a : Type} {motive : List a → Sort
   (F_1 : (t : List a) → List.below t → motive t), List.brecOn t F_1 = F_1 t (List.brecOn.go t F_1).2
 ```
 -/
-def mkBRecOnFromRec (recName : Name) (nParams : Nat)
+private def mkBRecOnFromRec (recName : Name) (nParams : Nat)
     (all : Array Name) (brecOnName : Name) : MetaM Unit := do
   let brecOnGoName := brecOnName.str "go"
   let brecOnEqName := brecOnName.str "eq"

src/Lean/Meta/Constructions/SparseCasesOn.lean

@@ -15,7 +15,7 @@ import Lean.Meta.Transform
 namespace Lean.Meta
 
 
-structure SparseCasesOnKey where
+private structure SparseCasesOnKey where
   indName : Name
   ctors   : Array Name
   -- When this is created in a private context and thus may contain private references, we must
@@ -23,7 +23,7 @@ structure SparseCasesOnKey where
   isPrivate : Bool
 deriving BEq, Hashable
 
-builtin_initialize sparseCasesOnCacheExt : EnvExtension (PHashMap SparseCasesOnKey Name) ←
+private builtin_initialize sparseCasesOnCacheExt : EnvExtension (PHashMap SparseCasesOnKey Name) ←
   registerEnvExtension (pure {}) (asyncMode := .local)  -- mere cache, keep it local
 
 /-- Information necessary to recognize and split on sparse casesOn (in particular in MatchEqs) -/
@@ -34,7 +34,7 @@ public structure SparseCasesOnInfo where
   insterestingCtors : Array Name
 deriving Inhabited
 
-builtin_initialize sparseCasesOnInfoExt : MapDeclarationExtension SparseCasesOnInfo ←
+private builtin_initialize sparseCasesOnInfoExt : MapDeclarationExtension SparseCasesOnInfo ←
   mkMapDeclarationExtension (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels

src/Lean/Meta/Constructions/SparseCasesOnEq.lean

@@ -83,7 +83,7 @@ where
           value := val
         })
 
-def isName (env : Environment) (n : Name) : Bool :=
+private def isName (env : Environment) (n : Name) : Bool :=
   if let .str p "else_eq" := n then
     (getSparseCasesOnInfoCore env p).isSome
   else

src/Lean/Meta/CtorIdxHInj.lean

@@ -16,7 +16,7 @@ def hinjSuffix := "hinj"
 public def mkCtorIdxHInjTheoremNameFor (indName : Name) : Name :=
   (mkCtorIdxName indName).str hinjSuffix
 
-partial def mkHInjectiveTheorem? (thmName : Name) (indVal : InductiveVal) : MetaM TheoremVal := do
+private partial def mkHInjectiveTheorem? (thmName : Name) (indVal : InductiveVal) : MetaM TheoremVal := do
   let us := indVal.levelParams.map mkLevelParam
   let thmType ←
     forallBoundedTelescope indVal.type (indVal.numParams + indVal.numIndices) fun xs1 _ => do

src/Lean/Meta/DecLevel.lean

@@ -69,16 +69,12 @@ def decLevel (u : Level) : MetaM Level := do
 
 /-- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`.
    Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level,
-   instantiate and normalize it, and then decrement 1 to obtain `u`. -/
+   and then decrement 1 to obtain `u`. -/
 def getDecLevel (type : Expr) : MetaM Level := do
-  let l ← getLevel type
-  let l ← normalizeLevel l
-  decLevel l
+  decLevel (← getLevel type)
 
 def getDecLevel? (type : Expr) : MetaM (Option Level) := do
-  let l ← getLevel type
-  let l ← normalizeLevel l
-  decLevel? l
+  decLevel? (← getLevel type)
 
 builtin_initialize
   registerTraceClass `Meta.isLevelDefEq.step

src/Lean/Meta/Match/AltTelescopes.lean

@@ -40,7 +40,7 @@ namespace Lean.Meta.Match
 
   This can be used to use the alternative of a match expression in its splitter.
 -/
-partial def forallAltVarsTelescope (altType : Expr) (altInfo : AltParamInfo)
+public partial def forallAltVarsTelescope (altType : Expr) (altInfo : AltParamInfo)
   (k : (patVars : Array Expr) → (args : Array Expr) → (mask : Array Bool) → (type : Expr) → MetaM α) : MetaM α := do
   assert! altInfo.numOverlaps = 0
   if altInfo.hasUnitThunk then
@@ -104,7 +104,7 @@ where
 
   This can be used to use the alternative of a match expression in its splitter.
 -/
-partial def forallAltTelescope (altType : Expr) (altInfo : AltParamInfo) (numDiscrEqs : Nat)
+public partial def forallAltTelescope (altType : Expr) (altInfo : AltParamInfo) (numDiscrEqs : Nat)
     (k : (ys : Array Expr) → (eqs : Array Expr) → (args : Array Expr) → (mask : Array Bool) → (type : Expr) → MetaM α)
     : MetaM α := do
   forallAltVarsTelescope altType altInfo fun ys args mask altType => do

src/Lean/Meta/Match/SolveOverlap.lean

@@ -21,7 +21,7 @@ We will eventually have to write more efficient proof automation for this module
 The new proof automation should exploit the structure of the generated goals and avoid general purpose tactics
 such as `contradiction`.
 -/
-def _root_.Lean.MVarId.contradictionQuick (mvarId : MVarId) : MetaM Bool := do
+private def _root_.Lean.MVarId.contradictionQuick (mvarId : MVarId) : MetaM Bool := do
   mvarId.withContext do
     let mut posMap : Std.HashMap Expr FVarId := {}
     let mut negMap : Std.HashMap Expr FVarId := {}

src/Lean/Meta/SizeOf.lean

@@ -149,15 +149,17 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
           trace[Meta.sizeOf] "declName: {declName}"
           trace[Meta.sizeOf] "type: {sizeOfType}"
           trace[Meta.sizeOf] "val: {sizeOfValue}"
-          addDecl <| Declaration.defnDecl {
-            name        := declName
-            levelParams := levelParams
-            type        := sizeOfType
-            value       := sizeOfValue
-            safety      := DefinitionSafety.safe
-            hints       := ReducibilityHints.abbrev
-          }
-          enableRealizationsForConst declName
+          -- We expose the `sizeOf` functions so that the `spec` theorems can be publicly `defeq`
+          withExporting do
+            addDecl <| Declaration.defnDecl {
+              name        := declName
+              levelParams := levelParams
+              type        := sizeOfType
+              value       := sizeOfValue
+              safety      := DefinitionSafety.safe
+              hints       := ReducibilityHints.abbrev
+            }
+            enableRealizationsForConst declName
 
 /--
   Create `sizeOf` functions for all inductive datatypes in the mutual inductive declaration containing `typeName`
@@ -451,24 +453,23 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
       let thmType ← mkForallFVars thmParams target
       trace[Meta.sizeOf] "sizeOf spec theorem name: {thmName}"
       trace[Meta.sizeOf] "sizeOf spec theorem type: {thmType}"
-      let thmValue ← withoutExporting do
-        let thmValue ← if indInfo.isNested then
-          SizeOfSpecNested.main lhs rhs |>.run {
-            indInfo, sizeOfFns, ctorName, params, localInsts, recMap
-          }
-        else
-          mkEqRefl rhs
-        let thmValue ← mkLambdaFVars thmParams thmValue
-        trace[Meta.sizeOf] "sizeOf spec theorem value: {thmValue}"
-        unless (← isDefEq (← inferType thmValue) thmType) do
-          throwError "type mismatch"
-        pure thmValue
+      let thmValue ← if indInfo.isNested then
+        SizeOfSpecNested.main lhs rhs |>.run {
+          indInfo, sizeOfFns, ctorName, params, localInsts, recMap
+        }
+      else
+        mkEqRefl rhs
+      let thmValue ← mkLambdaFVars thmParams thmValue
+      trace[Meta.sizeOf] "sizeOf spec theorem value: {thmValue}"
+      unless (← isDefEq (← inferType thmValue) thmType) do
+        throwError "type mismatch"
       addDecl <| Declaration.thmDecl {
         name        := thmName
         levelParams := ctorInfo.levelParams
         type        := thmType
         value       := thmValue
       }
+      inferDefEqAttr thmName
       simpAttr.add thmName default .global
       grindAttr.add thmName grindAttrStx .global
 

src/Lean/Meta/SplitSparseCasesOn.lean

@@ -16,7 +16,7 @@ import Lean.Meta.Tactic.Replace
 
 namespace Lean.Meta
 
-def rewriteGoalUsingEq (goal : MVarId) (eq : Expr) (symm : Bool := false) : MetaM MVarId := do
+private def rewriteGoalUsingEq (goal : MVarId) (eq : Expr) (symm : Bool := false) : MetaM MVarId := do
   let rewriteResult ← goal.rewrite (←goal.getType) eq symm
   goal.replaceTargetEq rewriteResult.eNew rewriteResult.eqProof
 

src/Lean/Meta/Sym/Simp/EvalGround.lean

@@ -383,7 +383,7 @@ When equal, uses `eq_self` (no kernel evaluation needed). When different, uses
 `mkStringLitNeProof` which finds the first differing character position and proves
 inequality via `congrArg (List.get?Internal · i)`.
 -/
-def evalStringEq (a b : Expr) : SimpM Result := do
+private def evalStringEq (a b : Expr) : SimpM Result := do
   let some va := getStringValue? a | return .rfl
   let some vb := getStringValue? b | return .rfl
   if va = vb then

src/Lean/Meta/Sym/Simp/SimpM.lean

@@ -172,7 +172,7 @@ inductive Result where
 Pre-computed `.rfl` results to avoid dynamic memory allocation.
 Each combination of `done` and `contextDependent` maps to a compile-time constant.
 -/
-def mkRflResult (done : Bool := false) (contextDependent : Bool := false) : Result :=
+public def mkRflResult (done : Bool := false) (contextDependent : Bool := false) : Result :=
   match done, contextDependent with
   | false, false => .rfl
   | false, true  => .rfl false true
@@ -180,15 +180,15 @@ def mkRflResult (done : Bool := false) (contextDependent : Bool := false) : Resu
   | true,  true  => .rfl true true
 
 /-- Like `mkRflResult` with `done := false`. -/
-def mkRflResultCD (contextDependent : Bool) : Result :=
+public def mkRflResultCD (contextDependent : Bool) : Result :=
   if contextDependent then .rfl false true else .rfl
 
 /-- Returns `true` if this result depends on the local context (e.g., hypotheses). -/
-abbrev Result.isContextDependent : Result → Bool
+public abbrev Result.isContextDependent : Result → Bool
   | .rfl _ cd | .step _ _ _ cd => cd
 
 /-- Marks a result as context-dependent. -/
-def Result.withContextDependent : Result → Result
+public def Result.withContextDependent : Result → Result
   | .rfl done _ => .rfl done true
   | .step e h done _ => .step e h done true
 

src/Lean/Meta/Sym/SymM.lean

@@ -66,7 +66,7 @@ This is used during pattern matching and structural definitional equality tests
 to identify arguments that can be skipped or handled specially
 (e.g., instance arguments can be synthesized, proof arguments can be inferred).
 -/
-structure ProofInstArgInfo where
+public structure ProofInstArgInfo where
   /-- `true` if this argument is a proof (its type is a `Prop`). -/
   isProof    : Bool
   /-- `true` if this argument is a type class instance. -/
@@ -78,7 +78,7 @@ Information about a function symbol. It stores which argument positions are proo
 enabling optimizations during pattern matching and structural definitional equality tests
 such as skipping proof arguments or deferring instance synthesis.
 -/
-structure ProofInstInfo where
+public structure ProofInstInfo where
   /-- Information about each argument position. -/
   argsInfo : Array ProofInstArgInfo
   deriving Inhabited

src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/Array.lean

@@ -17,7 +17,7 @@ import Init.GetElem
 namespace Lean.Meta.Tactic.Cbv
 
 /-- Extract elements from an array literal (`Array.mk` applied to a list literal). -/
-def getArrayLitElems? (e : Expr) : Option <| Array Expr :=
+private def getArrayLitElems? (e : Expr) : Option <| Array Expr :=
   match_expr e with
   | Array.mk _ as => getListLitElems as
   | _ => none

src/Lean/Meta/Tactic/Cleanup.lean

@@ -12,7 +12,7 @@ import Lean.Meta.Tactic.Util
 
 namespace Lean.Meta
 
-partial def cleanupCore (mvarId : MVarId) (toPreserve : Array FVarId) (indirectProps : Bool) : MetaM MVarId := do
+private partial def cleanupCore (mvarId : MVarId) (toPreserve : Array FVarId) (indirectProps : Bool) : MetaM MVarId := do
   mvarId.withContext do
     mvarId.checkNotAssigned `cleanup
     let used ← collectUsed |>.run' (false, {})

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean

@@ -112,25 +112,6 @@ private def processInv (e inst a : Expr) : RingM Unit := do
       return ()
   pushNewFact <| mkApp3 (mkConst ``Grind.CommRing.inv_split [ring.u]) ring.type fieldInst a
 
-/--
-For each new variable `x` in a ring with `PowIdentity α p`,
-push the equation `x ^ p = x` as a new fact into grind.
--/
-private def processPowIdentityVars : RingM Unit := do
-  let ring ← getCommRing
-  let some (powIdentityInst, csInst, p) := ring.powIdentityInst? | return ()
-  let startIdx := ring.powIdentityVarCount
-  let vars := ring.toRing.vars
-  if startIdx >= vars.size then return ()
-  for i in [startIdx:vars.size] do
-    let x := vars[i]!
-    trace_goal[grind.ring] "PowIdentity: pushing x^{p} = x for {x}"
-    -- Construct proof: @PowIdentity.pow_eq α csInst p powIdentityInst x
-    let proof := mkApp5 (mkConst ``Grind.PowIdentity.pow_eq [ring.u])
-      ring.type csInst (mkNatLit p) powIdentityInst x
-    pushNewFact proof
-  modifyCommRing fun s => { s with powIdentityVarCount := vars.size }
-
 /-- Returns `true` if `e` is a term `a⁻¹`. -/
 private def internalizeInv (e : Expr) : GoalM Bool := do
   match_expr e with
@@ -157,7 +138,6 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
       denote := s.denote.insert { expr := e } re
       denoteEntries := s.denoteEntries.push (e, re)
     }
-    processPowIdentityVars
   else if let some semiringId ← getCommSemiringId? type then SemiringM.run semiringId do
     let some re ← sreify? e | return ()
     trace_goal[grind.ring.internalize] "semiring [{semiringId}]: {e}"

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -38,13 +38,11 @@ where
     let noZeroDivInst? ← getNoZeroDivInst? u type
     trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
     let fieldInst? ← synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
-    let powIdentityInst? ← getPowIdentityInst? u type
-    trace_goal[grind.ring] "PowIdentity available: {powIdentityInst?.isSome}"
     let semiringId? := none
     let id := (← get').rings.size
     let ring : CommRing := {
       id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-      commRingInst, charInst?, noZeroDivInst?, fieldInst?, powIdentityInst?,
+      commRingInst, charInst?, noZeroDivInst?, fieldInst?,
     }
     modify' fun s => { s with rings := s.rings.push ring }
     return some id

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean

@@ -214,8 +214,6 @@ structure CommRing extends Ring where
   noZeroDivInst? : Option Expr
   /-- `Field` instance for `type` if available. -/
   fieldInst?     : Option Expr
-  /-- `PowIdentity` instance, the synthesized `CommSemiring` instance, and exponent `p` if available. -/
-  powIdentityInst? : Option (Expr × Expr × Nat) := none
   /-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal. -/
   denoteEntries  : PArray (Expr × RingExpr) := {}
   /-- Next unique id for `EqCnstr`s. -/
@@ -240,8 +238,6 @@ structure CommRing extends Ring where
   recheck        : Bool := false
   /-- Inverse theorems that have been already asserted. -/
   invSet         : PHashSet Expr := {}
-  /-- Number of variables for which `PowIdentity` equations have been pushed. -/
-  powIdentityVarCount : Nat := 0
   /--
   An equality of the form `c = 0`. It is used to simplify polynomial coefficients.
   -/

src/Lean/Meta/Tactic/Grind/Arith/Insts.lean

@@ -19,20 +19,6 @@ def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : GoalM (Opti
   let some n ← evalNat? n | return none
   return some (charInst, n)
 
-def getPowIdentityInst? (u : Level) (type : Expr) : GoalM (Option (Expr × Expr × Nat)) := do withNewMCtxDepth do
-  -- We use a fresh metavar for `CommSemiring` (unlike `getIsCharInst?` which pins the semiring)
-  -- because `PowIdentity` instances may be declared against a canonical `CommSemiring` instance
-  -- that is not definitionally equal to `CommRing.toCommSemiring`. The synthesized `csInst` is
-  -- stored and used in proof terms to ensure type-correctness.
-  let csInst ← mkFreshExprMVar (mkApp (mkConst ``Grind.CommSemiring [u]) type)
-  let p ← mkFreshExprMVar (mkConst ``Nat)
-  let powIdentityType := mkApp3 (mkConst ``Grind.PowIdentity [u]) type csInst p
-  let some inst ← synthInstance? powIdentityType | return none
-  let csInst ← instantiateMVars csInst
-  let p ← instantiateMVars p
-  let some pVal ← evalNat? p | return none
-  return some (inst, csInst, pVal)
-
 def getNoZeroDivInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
   let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
   let some natModuleInst ← synthInstance? natModuleType | return none

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -50,18 +50,6 @@ register_builtin_option debug.tactic.simp.checkDefEqAttr : Bool := {
     of the `defeq` attribute, and warn if it was. Note that this is a costly check."
 }
 
-register_builtin_option warning.simp.varHead : Bool := {
-  defValue := false
-  descr := "If true, warns when the head symbol of the left-hand side of a `@[simp]` theorem \
-    is a variable. Such lemmas are tried on every simp step, which can be slow."
-}
-
-register_builtin_option warning.simp.otherHead : Bool := {
-  defValue := true
-  descr := "If true, warns when the left-hand side of a `@[simp]` theorem is headed by a \
-    `.other` key in the discrimination tree (e.g. a lambda expression). Such lemmas can cause slowdowns."
-}
-
 /--
 An `Origin` is an identifier for simp theorems which indicates roughly
 what action the user took which lead to this theorem existing in the simp set.
@@ -371,27 +359,12 @@ private def checkTypeIsProp (type : Expr) : MetaM Unit :=
   unless (← isProp type) do
     throwError "Invalid simp theorem: Expected a proposition, but found{indentExpr type}"
 
-private def mkSimpTheoremKeys (type : Expr) (noIndexAtArgs : Bool) (checkLhs : Bool := false) : MetaM (Array SimpTheoremKey × Bool) := do
+private def mkSimpTheoremKeys (type : Expr) (noIndexAtArgs : Bool) : MetaM (Array SimpTheoremKey × Bool) := do
   withNewMCtxDepth do
     let (_, _, type) ← forallMetaTelescopeReducing type
     let type ← whnfR type
     match type.eq? with
-    | some (_, lhs, rhs) =>
-      let keys ← DiscrTree.mkPath lhs noIndexAtArgs
-      if checkLhs then
-        if warning.simp.varHead.get (← getOptions) && keys[0]? == some .star then
-          logWarning m!"Left-hand side of simp theorem has a variable as head symbol. \
-            This means the theorem will be tried on every simp step, which can be expensive. \
-            This may be acceptable for `local` or `scoped` simp lemmas.\n\
-            Use `set_option warning.simp.varHead false` to disable this warning."
-        if warning.simp.otherHead.get (← getOptions) && keys[0]? == some .other then
-          logWarning m!"Left-hand side of simp theorem is headed by a `.other` key in the \
-            discrimination tree (e.g. because it is a lambda expression). \
-            This theorem will be tried against all expressions that also have a `.other` key as head, \
-            which can cause slowdowns. \
-            This may be acceptable for `local` or `scoped` simp lemmas.\n\
-            Use `set_option warning.simp.otherHead false` to disable this warning."
-      pure (keys, ← isPerm lhs rhs)
+    | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs)
     | none => throwError "Unexpected kind of simp theorem{indentExpr type}"
 
 register_builtin_option simp.rfl.checkTransparency: Bool := {
@@ -400,19 +373,19 @@ register_builtin_option simp.rfl.checkTransparency: Bool := {
 }
 
 private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr)
-    (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) (checkLhs : Bool := false): MetaM SimpTheorem := do
+    (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) : MetaM SimpTheorem := do
   assert! origin != .fvar ⟨.anonymous⟩
   let type ← instantiateMVars (← inferType e)
-  let (keys, perm) ← mkSimpTheoremKeys type noIndexAtArgs checkLhs
+  let (keys, perm) ← mkSimpTheoremKeys type noIndexAtArgs
   let rfl ← isRflProof proof
   if rfl && simp.rfl.checkTransparency.get (← getOptions) then
     forallTelescopeReducing type fun _ type => do
       let checkDefEq (lhs rhs : Expr) := do
         unless (← withTransparency .instances <| isDefEq lhs rhs) do
-          logWarning m!"`{origin.key}` is a `[defeq]` simp theorem, but its left-hand side{indentExpr lhs}\n\
+          logWarning m!"`{origin.key}` is a `rfl` simp theorem, but its left-hand side{indentExpr lhs}\n\
             is not definitionally equal to the right-hand side{indentExpr rhs}\n\
             at `.instances` transparency. Possible solutions:\n\
-            1- use `(rfl)` as the proof\n\
+            1- use `id rfl` as the proof\n\
             2- mark constants occurring in the lhs and rhs as `[implicit_reducible]`"
       match_expr type with
       | Eq _ lhs rhs => checkDefEq lhs rhs
@@ -426,7 +399,7 @@ Creates a `SimpTheorem` from a global theorem.
 Because some theorems lead to multiple `SimpTheorems` (in particular conjunctions), returns an array.
 -/
 def mkSimpTheoremFromConst (declName : Name) (post := true) (inv := false)
-    (prio : Nat := eval_prio default) (checkLhs : Bool := false) : MetaM (Array SimpTheorem) := do
+    (prio : Nat := eval_prio default) : MetaM (Array SimpTheorem) := do
   let cinfo ← getConstVal declName
   let us := cinfo.levelParams.map mkLevelParam
   let origin := .decl declName post inv
@@ -440,10 +413,10 @@ def mkSimpTheoremFromConst (declName : Name) (post := true) (inv := false)
         let auxName ← mkAuxLemma (kind? := `_simp) cinfo.levelParams type val (inferRfl := true)
           (forceExpose := true)  -- These kinds of theorems are small and `to_additive` may need to
                                  -- unfold them.
-        r := r.push <| (← do mkSimpTheoremCore origin (mkConst auxName us) #[] (mkConst auxName) post prio (noIndexAtArgs := false) (checkLhs := checkLhs))
+        r := r.push <| (← do mkSimpTheoremCore origin (mkConst auxName us) #[] (mkConst auxName) post prio (noIndexAtArgs := false))
       return r
     else
-      return #[← withoutExporting do mkSimpTheoremCore origin (mkConst declName us) #[] (mkConst declName) post prio (noIndexAtArgs := false) (checkLhs := checkLhs)]
+      return #[← withoutExporting do mkSimpTheoremCore origin (mkConst declName us) #[] (mkConst declName) post prio (noIndexAtArgs := false)]
 
 def SimpTheorem.getValue (simpThm : SimpTheorem) : MetaM Expr := do
   if simpThm.proof.isConst && simpThm.levelParams.isEmpty then
@@ -697,7 +670,7 @@ def SimpExtension.getTheorems (ext : SimpExtension) : CoreM SimpTheorems :=
 Adds a simp theorem to a simp extension
 -/
 def addSimpTheorem (ext : SimpExtension) (declName : Name) (post : Bool) (inv : Bool) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
-  let simpThms ← withExporting (isExporting := attrKind != .local && !isPrivateName declName) do mkSimpTheoremFromConst declName post inv prio (checkLhs := true)
+  let simpThms ← withExporting (isExporting := attrKind != .local && !isPrivateName declName) do mkSimpTheoremFromConst declName post inv prio
   for simpThm in simpThms do
     ext.add (SimpEntry.thm simpThm) attrKind
 

src/Lean/Meta/WrapInstance.lean

@@ -9,8 +9,8 @@ prelude
 public import Lean.Meta.Closure
 public import Lean.Meta.SynthInstance
 public import Lean.Meta.CtorRecognizer
-public import Lean.Meta.AppBuilder
-import Lean.Structure
+
+public section
 
 /-!
 # Instance Wrapping
@@ -25,30 +25,22 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 `wrapInstance` constructs a result instance as follows, executing all steps at
 `instances` transparency:
 
-1. If `I'` is not a class application, return `i` unchanged.
+1. If `I'` is not a class, return `i` unchanged.
 2. If `I'` is a proposition, wrap `i` in an auxiliary theorem of type `I'` and return it
    (controlled by `backward.inferInstanceAs.wrap.instances`).
 3. Reduce `i` to whnf.
-4. If `i` is not a constructor application: if `I` is already defeq to `I'`,
+4. If `i` is not a constructor application: if the type of `i` is already defeq to `I'`,
    return `i`; otherwise wrap it in an auxiliary definition of type `I'` and return it
    (controlled by `backward.inferInstanceAs.wrap.instances`).
-5. Otherwise, if `i` is an application of `ctor` of class `C`:
-   - Unify the conclusion of the type of `ctor` with `I'` to obtain adjusted field type `Fᵢ'` for
-     each field.
-   - Return a new application `ctor ... : I'` where the fields are adjusted as follows:
+5. Otherwise, for `i = ctor a₁ ... aₙ` with `ctor : C ?p₁ ... ?pₙ`:
+   - Unify `C ?p₁ ... ?pₙ` with `I'`.
+   - Return a new application `ctor a₁' ... aₙ' : I'` where each `aᵢ'` is constructed as:
      - If the field type is a proposition: assign directly if types are defeq, otherwise
        wrap in an auxiliary theorem.
-     - If the field is a parent field (subobject) `p : P`: first try to reuse an existing
-       instance that can be synthesized for `P` (controlled by
-       `backward.inferInstanceAs.wrap.reuseSubInstances`) in order to preserve defeqs; if that
-       fails, recurse.
-     - If it is a field of a flattened parent class `C'` and
-       `backward.inferInstanceAs.wrap.reuseSubInstances` is true, try synthesizing an instance of
-       `C'` for `I'` and if successful, use the corresponding projection of the found instance in
-       order to preserve defeqs; otherwise, continue.
-       - Specifically, construct the chain of base projections from `C` to `C'` applied to `_ : I'`
-         and infer its type to obtain an appropriate application of `C'` for the instance search.
-     - Otherwise (non-inherited data field): assign directly if types are defeq, otherwise wrap in an
+     - If the field type is a class: first try to reuse an existing synthesized instance
+       for the target type (controlled by `backward.inferInstanceAs.wrap.reuseSubInstances`);
+       if that fails, recurse with source instance `aᵢ` and expected type `?pᵢ`.
+     - Otherwise (data field): assign directly if types are defeq, otherwise wrap in an
        auxiliary definition to fix the type (controlled by `backward.inferInstanceAs.wrap.data`).
 
 ## Options
@@ -64,62 +56,48 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 
 namespace Lean.Meta
 
-public register_builtin_option backward.inferInstanceAs.wrap : Bool := {
+register_builtin_option backward.inferInstanceAs.wrap : Bool := {
   defValue := true
   descr := "wrap instance bodies in `inferInstanceAs` and the default `deriving` handler"
 }
 
-public register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
+register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
   defValue := true
   descr := "when recursing into sub-instances, reuse existing instances for the target type instead of re-wrapping them, which can be important to avoid non-defeq instance diamonds"
 }
 
-public register_builtin_option backward.inferInstanceAs.wrap.instances : Bool := {
+register_builtin_option backward.inferInstanceAs.wrap.instances : Bool := {
   defValue := true
   descr := "wrap non-reducible instances in auxiliary definitions to fix their types"
 }
 
-public register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
+register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
   defValue := true
   descr := "wrap data fields in auxiliary definitions to fix their types"
 }
 
 builtin_initialize registerTraceClass `Meta.wrapInstance
 
-open Meta
-
-partial def getFieldOrigin (structName field : Name) : MetaM (Name × StructureFieldInfo) := do
-  let env ← getEnv
-  for parent in getStructureParentInfo env structName do
-    if (findField? env parent.structName field).isSome then
-      return ← getFieldOrigin parent.structName field
-  let some fi := getFieldInfo? env structName field
-    | throwError "no such field {field} in {structName}"
-  return (structName, fi)
-
-/-- Projects application of a structure type to corresponding application of a parent structure. -/
-def getParentStructType? (structName parentStructName : Name) (structType : Expr) : MetaM (Option Expr) := OptionT.run do
-  let env ← getEnv
-  let some path := getPathToBaseStructure? env parentStructName structName | failure
-  withLocalDeclD `self structType fun self => do
-    let proj ← path.foldlM (init := self) fun e projFn => do
-      let ty ← whnf (← inferType e)
-      let .const _ us := ty.getAppFn
-        | trace[Meta.wrapInstance] "could not reduce type `{ty}`"
-          failure
-      let params := ty.getAppArgs
-      pure <| mkApp (mkAppN (.const projFn us) params) e
-    let projTy ← whnf <| ← inferType proj
-    if projTy.containsFVar self.fvarId! then
-      trace[Meta.wrapInstance] "parent type depends on instance fields{indentExpr projTy}"
-      failure
-    return projTy
+/--
+Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
+Non-instance-implicit arguments are assigned from the original application's arguments.
+If the function is over-applied, extra arguments are preserved.
+-/
+def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
+  let fn := type.getAppFn
+  let args := type.getAppArgs
+  let (mvars, bis, _) ← forallMetaTelescope (← inferType fn)
+  for i in [:mvars.size] do
+    unless bis[i]!.isInstImplicit do
+      mvars[i]!.mvarId!.assign args[i]!
+  let args := mvars ++ args.drop mvars.size
+  instantiateMVars (mkAppN fn args)
 
 /--
 Wrap an instance value so its type matches the expected type exactly.
 See the module docstring for the full algorithm specification.
 -/
-public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
+partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
     (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
   withTraceNode `Meta.wrapInstance
       (fun _ => return m!"type: {expectedType}") do
@@ -134,7 +112,8 @@ public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := tr
       return inst
 
   -- Try to reduce it to a constructor.
-  (← whnf inst).withApp fun f args => do
+  let inst ← whnf inst
+  inst.withApp fun f args => do
     let some (.ctorInfo ci) ← f.constName?.mapM getConstInfo
       | do
         trace[Meta.wrapInstance] "did not reduce to constructor application, returning/wrapping as is: {inst}"
@@ -177,10 +156,8 @@ public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := tr
           else
             trace[Meta.wrapInstance] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
             mvarId.assign (← mkAuxTheorem argExpectedType arg (zetaDelta := true))
-          continue
-
         -- Recurse into instance arguments of the constructor
-        if (← isClass? argExpectedType).isSome then
+        else if (← isClass? argExpectedType).isSome then
           if backward.inferInstanceAs.wrap.reuseSubInstances.get (← getOptions) then
             -- Reuse existing instance for the target type if any. This is especially important when recursing
             -- as it guarantees subinstances of overlapping instances are defeq under more than just
@@ -194,35 +171,22 @@ public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := tr
 
           mvarId.assign (← wrapInstance arg argExpectedType (compile := compile)
             (logCompileErrors := logCompileErrors) (isMeta := isMeta))
-          continue
-
-        if backward.inferInstanceAs.wrap.reuseSubInstances.get (← getOptions) then
-          let (baseClassName, fieldInfo) ← getFieldOrigin className mvarDecl.userName
-          if baseClassName != className then
-            trace[Meta.wrapInstance] "found inherited field `{mvarDecl.userName}` from parent `{baseClassName}`"
-            if let some baseClassType ← getParentStructType? className baseClassName expectedType then
-              try
-                if let .some existingBaseClassInst ← trySynthInstance baseClassType then
-                  trace[Meta.wrapInstance] "using projection of existing instance `{existingBaseClassInst}`"
-                  mvarId.assign (← mkProjection existingBaseClassInst fieldInfo.fieldName)
-                  continue
-                trace[Meta.wrapInstance] "did not find existing instance for `{baseClassName}`"
-              catch e =>
-                trace[Meta.wrapInstance] "error when attempting to reuse existing instance for `{baseClassName}`: {e.toMessageData}"
-
-        -- For data fields, assign directly or wrap in aux def to fix types.
-        if backward.inferInstanceAs.wrap.data.get (← getOptions) then
-          let argType ← inferType arg
-          if ← isDefEq argExpectedType argType then
-            mvarId.assign arg
-          else
-            let name ← mkAuxDeclName
-            mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
-            setInlineAttribute name
-            if isMeta then modifyEnv (markMeta · name)
-            if compile then
-              compileDecls (logErrors := logCompileErrors) #[name]
-            enableRealizationsForConst name
         else
-          mvarId.assign arg
+          -- For data fields, assign directly or wrap in aux def to fix types.
+          if backward.inferInstanceAs.wrap.data.get (← getOptions) then
+            let argType ← inferType arg
+            if ← isDefEq argExpectedType argType then
+              mvarId.assign arg
+            else
+              let name ← mkAuxDeclName
+              mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
+              setInlineAttribute name
+              if isMeta then modifyEnv (markMeta · name)
+              if compile then
+                compileDecls (logErrors := logCompileErrors) #[name]
+              enableRealizationsForConst name
+          else
+            mvarId.assign arg
       return mkAppN f (← mvars.mapM instantiateMVars)
+
+end Lean.Meta

src/Lean/Parser/Basic.lean

@@ -1115,6 +1115,11 @@ def symbolNoAntiquot (sym : String) : Parser :=
   { info := symbolInfo sym
     fn   := symbolFn sym }
 
+def checkTailNoWs (prev : Syntax) : Bool :=
+  match prev.getTailInfo with
+  | .original _ _ trailing _ => trailing.stopPos == trailing.startPos
+  | _                        => false
+
 /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
     parsing local tokens that have not been added to the token table (but may have
     been so by some unrelated code).
@@ -1163,18 +1168,13 @@ partial def strAux (sym : String) (errorMsg : String) (j : String.Pos.Raw) :Pars
       else parse (j.next' sym h₁) c (s.next' c i h₂)
   parse j
 
-private def pickNonNone (stack : SyntaxStack) : Syntax :=
-  match stack.toSubarray.findRev? fun stx => !stx.isNone with
-  | none => Syntax.missing
-  | some stx => stx
-
 def checkTailWs (prev : Syntax) : Bool :=
   match prev.getTailInfo with
   | .original _ _ trailing _ => trailing.stopPos > trailing.startPos
   | _                        => false
 
 def checkWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
-  let prev := pickNonNone s.stxStack
+  let prev := s.stxStack.back
   if checkTailWs prev then s else s.mkError errorMsg
 
 /-- The `ws` parser requires that there is some whitespace at this location.
@@ -1202,10 +1202,10 @@ This parser has arity 0 - it does not capture anything. -/
   info := epsilonInfo
   fn   := checkLinebreakBeforeFn errorMsg
 
-def checkTailNoWs (prev : Syntax) : Bool :=
-  match prev.getTailInfo with
-  | .original _ _ trailing _ => trailing.stopPos == trailing.startPos
-  | _                        => false
+private def pickNonNone (stack : SyntaxStack) : Syntax :=
+  match stack.toSubarray.findRev? fun stx => !stx.isNone with
+  | none => Syntax.missing
+  | some stx => stx
 
 def checkNoWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
   let prev := pickNonNone s.stxStack

src/Lean/Parser/Command.lean

@@ -122,9 +122,7 @@ def declModifiers (inline : Bool) := leading_parser
 /-- `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names -/
 -- @[builtin_doc] -- FIXME: suppress the hover
 def declId := leading_parser
-  ident >>
-  optional (checkNoWsBefore "no space before '.{'" >> ".{" >>
-    sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
+  ident >> optional (".{" >> sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
 /-- `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` -/
 -- @[builtin_doc] -- FIXME: suppress the hover
 def declSig := leading_parser
@@ -342,11 +340,10 @@ namespace InternalSyntax
   This command is for internal use only. It is intended for macros that implicitly introduce new
   scopes, such as `expandInCmd` and `expandNamespacedDeclaration`. It allows local attributes to remain
   accessible beyond those implicit scopes, even though they would normally be hidden from the user.
-  The numeric argument specifies how many scope levels to mark as non-delimiting.
   -/
-  scoped syntax (name := end_local_scope) "end_local_scope" num : command
+  scoped syntax (name := end_local_scope) "end_local_scope" : command
 
-  def endLocalScopeSyntax (depth : Nat) : Command := Unhygienic.run `(end_local_scope $(Syntax.mkNumLit (toString depth)))
+  def endLocalScopeSyntax : Command := Unhygienic.run `(end_local_scope)
 end InternalSyntax
 
 /-- Declares one or more typed variables, or modifies whether already-declared variables are

src/Lean/Parser/Do.lean

@@ -66,14 +66,6 @@ def notFollowedByRedefinedTermToken :=
       "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
-namespace InternalSyntax
-/--
-Internal syntax used in the `if` and `unless` elaborators. Behaves like `pure PUnit.unit` but
-uses `()` if possible and gives better error messages.
--/
-scoped syntax (name := doSkip) "skip" : doElem
-end InternalSyntax
-
 @[builtin_doElem_parser] def doLet      := leading_parser
   "let " >> optional "mut " >> letConfig >> letDecl
 @[builtin_doElem_parser] def doLetElse  := leading_parser withPosition <|

src/Lean/Parser/Module.lean

@@ -127,10 +127,7 @@ private def consumeInput (inputCtx : InputContext) (pmctx : ParserModuleContext)
   | none   => s.pos
 
 def topLevelCommandParserFn : ParserFn :=
-  -- set position to enforce appropriate indentation of applications etc.
-  -- We don't do it for nested commands such as in quotations where
-  -- formatting might be less rigid.
-  (withPosition commandParser).fn
+  commandParser.fn
 
 partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext) (mps : ModuleParserState) (messages : MessageLog) : Syntax × ModuleParserState × MessageLog := Id.run do
   let mut pos := mps.pos

src/Lean/Parser/Term.lean

@@ -50,17 +50,17 @@ def versoCommentBodyFn : ParserFn := fun c s =>
     rawFn (Doc.Parser.ignoreFn <| chFn '-' >> chFn '/') (trailingWs := true) c s
   else s
 
-def versoCommentBody : Parser where
+public def versoCommentBody : Parser where
   fn := fun c s => nodeFn `Lean.Parser.Command.versoCommentBody versoCommentBodyFn c s
 
 
 @[combinator_parenthesizer versoCommentBody, expose]
-def versoCommentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
+public def versoCommentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
 
 open PrettyPrinter Formatter in
 open Syntax.MonadTraverser in
 @[combinator_formatter versoCommentBody, expose]
-def versoCommentBody.formatter : PrettyPrinter.Formatter := do
+public def versoCommentBody.formatter : PrettyPrinter.Formatter := do
   visitArgs $ do
     visitAtom `«-/»
     goLeft
@@ -354,13 +354,6 @@ def structInstFieldDef := leading_parser
 def structInstFieldEqns := leading_parser
   optional "private" >> matchAlts
 
-/--
-Synthesizes a default value for a structure, making use of `Inhabited` instances for
-missing fields, as well as `Inhabited` instances for parent structures.
--/
-@[builtin_term_parser] def structInstDefault := leading_parser
-  "struct_inst_default%"
-
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
   atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
 def funStrictImplicitBinder :=
@@ -896,21 +889,14 @@ def isIdent (stx : Syntax) : Bool :=
   -- antiquotations should also be allowed where an identifier is expected
   stx.isAntiquot || stx.isIdent
 
-/-- Predicate for what `explicitUniv` can follow. It is only meant to be used on an identifier
-that becomes the head constant of an application. -/
-def isIdentOrDotIdentOrProj (stx : Syntax) : Bool :=
-  isIdent stx || stx.isOfKind ``dotIdent || stx.isOfKind ``proj
+def isIdentOrDotIdent (stx : Syntax) : Bool :=
+  isIdent stx || stx.isOfKind ``dotIdent
 
-/-- Syntax for `.{u, ...}` itself. Generally the `explicitUniv` trailing parser suffices.
-However, for `e |>.x.{u} a1 a2 a3` notation we need to be able to express explicit universes in the
-middle of the syntax. -/
-def explicitUnivSuffix : Parser :=
-  checkNoWsBefore "no space before '.{'" >> ".{" >>
-  sepBy1 levelParser ", " >> "}"
 /-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
 @[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
-  checkStackTop isIdentOrDotIdentOrProj "expected preceding identifier" >>
-  explicitUnivSuffix
+  checkStackTop isIdentOrDotIdent "expected preceding identifier" >>
+  checkNoWsBefore "no space before '.{'" >> ".{" >>
+  sepBy1 levelParser ", " >> "}"
 /-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
 If present, the identifier `h` is bound to a proof of `x = e`. -/
 @[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser
@@ -923,7 +909,7 @@ If present, the identifier `h` is bound to a proof of `x = e`. -/
 It is especially useful for avoiding parentheses with repeated applications.
 -/
 @[builtin_term_parser] def pipeProj   := trailing_parser:minPrec
-  " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> optional explicitUnivSuffix >> many argument
+  " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
 @[builtin_term_parser] def pipeCompletion := trailing_parser:minPrec
   " |>."
 

src/Lean/Parser/Term/Basic.lean

@@ -84,12 +84,11 @@ Delimiter-free indentation is determined by the *first* tactic of the sequence.
   tacticSeqBracketed <|> tacticSeq1Indented
 
 /-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation.
-Falls back to an empty tactic sequence when no appropriately indented content follows, producing
-an elaboration error (unsolved goals) rather than a parse error. -/
+The strict indentation requirement only apply to *nested* `by`s, as top-level `by`s do not have a
+position set. -/
 @[builtin_doc, run_builtin_parser_attribute_hooks]
 def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
-  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented) <|>
-  node ``tacticSeq1Indented pushNone
+  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented)
 
 /- Raw sequence for quotation and grouping -/
 @[run_builtin_parser_attribute_hooks]