.

This PR adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in #6189 now incentivizes.

Closes the already closed #2524

CODEOWNERS

@@ -4,7 +4,7 @@
 # Listed persons will automatically be asked by GitHub to review a PR touching these paths.
 # If multiple names are listed, a review by any of them is considered sufficient by default.
 
-/.github/ @Kha @kim-em
+/.github/ @kim-em
 /RELEASES.md @kim-em
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
@@ -14,9 +14,7 @@
 /src/Lean/Elab/Tactic/ @kim-em
 /src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
-/src/Lean/Parser/ @Kha
-/src/Lean/PrettyPrinter/ @Kha
-/src/Lean/PrettyPrinter/Delaborator/ @kmill
+/src/Lean/PrettyPrinter/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
 /src/Init/Data/ @kim-em

src/Init/Data/Array/Lemmas.lean

@@ -19,8 +19,6 @@ import Init.Data.List.ToArray
 ## Theorems about `Array`.
 -/
 
-
-
 namespace Array
 
 /-! ## Preliminaries -/
@@ -184,6 +182,14 @@ theorem getElem_eq_getElem?_get (a : Array α) (i : Nat) (h : i < a.size) :
     a[i] = a[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
+theorem getD_getElem? (a : Array α) (i : Nat) (d : α) :
+    a[i]?.getD d = if p : i < a.size then a[i]'p else d := by
+  if h : i < a.size then
+    simp [h, getElem?_def]
+  else
+    have p : i ≥ a.size := Nat.le_of_not_gt h
+    simp [getElem?_eq_none p, h]
+
 @[simp] theorem getElem?_empty {n : Nat} : (#[] : Array α)[n]? = none := rfl
 
 theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
@@ -710,6 +716,164 @@ theorem all_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
     (l.push a).contains b = (l.contains b || b == a) := by
   simp [contains]
 
+/-! ### set -/
+
+
+/-! # set -/
+
+@[simp] theorem getElem_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
+      (eq : i = j) (p : j < (a.set i v).size) :
+    (a.set i v)[j]'p = v := by
+  cases a
+  simp
+  simp [set, ← getElem_toList, ←eq]
+
+@[deprecated getElem_set_self (since := "2024-12-11")]
+abbrev getElem_set_eq := @getElem_set_self
+
+@[simp] theorem getElem?_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
+    (a.set i v)[i]? = v := by simp [getElem?_eq_getElem, h]
+
+@[deprecated getElem?_set_self (since := "2024-12-11")]
+abbrev getElem?_set_eq := @getElem?_set_self
+
+@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
+    (pj : j < (a.set i v).size) (h : i ≠ j) :
+    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
+  simp only [set, ← getElem_toList, List.getElem_set_ne h]
+
+@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
+    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
+  by_cases h : j < a.size <;> simp [getElem?_eq_getElem, getElem?_eq_none, Nat.ge_of_not_lt, ne, h]
+
+theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
+    (h : j < (a.set i v).size) :
+    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
+  by_cases p : i = j <;> simp [p]
+
+theorem getElem?_set (a : Array α) (i : Nat) (h : i < a.size) (v : α) (j : Nat) :
+    (a.set i v)[j]? = if i = j then some v else a[j]? := by
+  split <;> simp_all
+
+@[simp] theorem set_getElem_self {as : Array α} {i : Nat} (h : i < as.size) :
+    as.set i as[i] = as := by
+  cases as
+  simp
+
+@[simp] theorem set_eq_empty_iff {as : Array α} (n : Nat) (a : α) (h) :
+     as.set n a = #[] ↔ as = #[] := by
+  cases as <;> cases n <;> simp [set]
+
+theorem set_comm (a b : α)
+    {n m : Nat} (as : Array α) {hn : n < as.size} {hm : m < (as.set n a).size} (h : n ≠ m) :
+    (as.set n a).set m b = (as.set m b (by simpa using hm)).set n a (by simpa using hn) := by
+  cases as
+  simp [List.set_comm _ _ _ h]
+
+@[simp]
+theorem set_set (a b : α) (as : Array α) (n : Nat) (h : n < as.size) :
+    (as.set n a).set n b (by simpa using h) = as.set n b := by
+  cases as
+  simp
+
+theorem mem_set (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
+    a ∈ as.set n a := by
+  simp [mem_iff_getElem]
+  exact ⟨n, (by simpa using h), by simp⟩
+
+theorem mem_or_eq_of_mem_set
+    {as : Array α} {n : Nat} {a b : α} {w : n < as.size} (h : a ∈ as.set n b) : a ∈ as ∨ a = b := by
+  cases as
+  simpa using List.mem_or_eq_of_mem_set (by simpa using h)
+
+/-! # setIfInBounds -/
+
+@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
+
+@[simp] theorem size_setIfInBounds (as : Array α) (index : Nat) (val : α) :
+    (as.setIfInBounds index val).size = as.size := by
+  if h : index < as.size  then
+    simp [setIfInBounds, h]
+  else
+    simp [setIfInBounds, h]
+
+theorem getElem_setIfInBounds (as : Array α) (i : Nat) (v : α) (j : Nat)
+    (hj : j < (as.setIfInBounds i v).size) :
+    (as.setIfInBounds i v)[j]'hj = if i = j then v else as[j]'(by simpa using hj) := by
+  simp only [setIfInBounds]
+  split
+  · simp [getElem_set]
+  · simp only [size_setIfInBounds] at hj
+    rw [if_neg]
+    omega
+
+@[simp] theorem getElem_setIfInBounds_self (as : Array α) {i : Nat} (v : α) (h : _) :
+    (as.setIfInBounds i v)[i]'h = v := by
+  simp at h
+  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_self]
+
+@[deprecated getElem_setIfInBounds_self (since := "2024-12-11")]
+abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
+
+@[simp] theorem getElem_setIfInBounds_ne (as : Array α) {i : Nat} (v : α) {j : Nat}
+    (hj : j < (as.setIfInBounds i v).size) (h : i ≠ j) :
+    (as.setIfInBounds i v)[j]'hj = as[j]'(by simpa using hj) := by
+  simp [getElem_setIfInBounds, h]
+
+@[simp]
+theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (p : i < as.size) (v : α) :
+    (as.setIfInBounds i v)[i]? = some v := by
+  simp [getElem?_eq_getElem, p]
+
+@[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
+abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self
+
+theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α}  :
+    (as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]? := by
+  cases as
+  simp [List.getElem?_set]
+
+@[simp] theorem getElem?_setIfInBounds_ne {as : Array α} {i j : Nat} (h : i ≠ j) {a : α}  :
+    (as.setIfInBounds i a)[j]? = as[j]? := by
+  simp [getElem?_setIfInBounds, h]
+
+theorem setIfInBounds_eq_of_size_le {l : Array α} {n : Nat} (h : l.size ≤ n) {a : α} :
+    l.setIfInBounds n a = l := by
+  cases l
+  simp [List.set_eq_of_length_le (by simpa using h)]
+
+@[simp] theorem setIfInBounds_eq_empty_iff {as : Array α} (n : Nat) (a : α) :
+     as.setIfInBounds n a = #[] ↔ as = #[] := by
+  cases as <;> cases n <;> simp
+
+theorem setIfInBounds_comm (a b : α)
+    {n m : Nat} (as : Array α) (h : n ≠ m) :
+    (as.setIfInBounds n a).setIfInBounds m b = (as.setIfInBounds m b).setIfInBounds n a := by
+  cases as
+  simp [List.set_comm _ _ _ h]
+
+@[simp]
+theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (n : Nat) :
+    (as.setIfInBounds n a).setIfInBounds n b = as.setIfInBounds n b := by
+  cases as
+  simp
+
+theorem mem_setIfInBounds (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
+    a ∈ as.setIfInBounds n a := by
+  simp [mem_iff_getElem]
+  exact ⟨n, (by simpa using h), by simp⟩
+
+theorem mem_or_eq_of_mem_setIfInBounds
+    {as : Array α} {n : Nat} {a b : α} (h : a ∈ as.setIfInBounds n b) : a ∈ as ∨ a = b := by
+  cases as
+  simpa using List.mem_or_eq_of_mem_set (by simpa using h)
+
+/-- Simplifies a normal form from `get!` -/
+@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
+    (setIfInBounds a i v)[i]?.getD d = if i < a.size then v else d := by
+  by_cases h : i < a.size <;>
+    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]
+
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
@@ -820,102 +984,31 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 
 /-! # get -/
 
+@[deprecated getElem?_eq_getElem (since := "2024-12-11")]
 theorem getElem?_lt
     (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
 
+@[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_ge
     (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
 
 @[simp] theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
 
+@[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none := by
-  simp [getElem?_ge, h]
+  simp [getElem?_eq_none, h]
 
-theorem getD_get? (a : Array α) (i : Nat) (d : α) :
-  Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
-  if h : i < a.size then
-    simp [setIfInBounds, h, getElem?_def]
-  else
-    have p : i ≥ a.size := Nat.le_of_not_gt h
-    simp [setIfInBounds, getElem?_len_le _ p, h]
+@[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
 
 @[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
-  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
+  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_getElem?, *]
 
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
 @[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
     a.get! i = (a.get? i).getD default := by
   by_cases p : i < a.size <;>
-  simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]
-
-/-! # set -/
-
-@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
-      (eq : i = j) (p : j < (a.set i v).size) :
-    (a.set i v)[j]'p = v := by
-  cases a
-  simp
-  simp [set, ← getElem_toList, ←eq]
-
-@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
-    (pj : j < (a.set i v).size) (h : i ≠ j) :
-    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
-  simp only [set, ← getElem_toList, List.getElem_set_ne h]
-
-theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
-    (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
-  by_cases p : i = j <;> simp [p]
-
-@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
-    (a.set i v)[i]? = v := by simp [getElem?_lt, h]
-
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
-    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
-  by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
-
-/-! # setIfInBounds -/
-
-@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
-
-@[simp] theorem size_setIfInBounds (a : Array α) (index : Nat) (val : α) :
-    (Array.setIfInBounds a index val).size = a.size := by
-  if h : index < a.size  then
-    simp [setIfInBounds, h]
-  else
-    simp [setIfInBounds, h]
-
-theorem getElem_setIfInBounds (a : Array α) (i : Nat) (v : α) (j : Nat)
-    (hj : j < (setIfInBounds a i v).size) :
-  (setIfInBounds a i v)[j]'hj = if i = j then v else a[j]'(by simpa using hj) := by
-  simp only [setIfInBounds]
-  split
-  · simp [getElem_set]
-  · simp only [size_setIfInBounds] at hj
-    rw [if_neg]
-    omega
-
-@[simp] theorem getElem_setIfInBounds_eq (a : Array α) {i : Nat} (v : α) (h : _) :
-    (setIfInBounds a i v)[i]'h = v := by
-  simp at h
-  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_eq]
-
-@[simp] theorem getElem_setIfInBounds_ne (a : Array α) {i : Nat} (v : α) {j : Nat}
-    (hj : j < (setIfInBounds a i v).size) (h : i ≠ j) :
-    (setIfInBounds a i v)[j]'hj = a[j]'(by simpa using hj) := by
-  simp [getElem_setIfInBounds, h]
-
-@[simp]
-theorem getElem?_setIfInBounds_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) :
-    (a.setIfInBounds i v)[i]? = some v := by
-  simp [getElem?_lt, p]
-
-/-- Simplifies a normal form from `get!` -/
-@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
-    Option.getD (setIfInBounds a i v)[i]? d = if i < a.size then v else d := by
-  by_cases h : i < a.size <;>
-    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_get?]
+  simp only [get!_eq_getD, getD_eq_get?, getD_getElem?, p, get?_eq_getElem?]
 
 /-! # ofFn -/
 
@@ -1092,9 +1185,6 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
     (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, ← getElem_toList, List.getElem_set_ne h]
 
-theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
-    (a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
-
 private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
 
 theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
@@ -1998,14 +2088,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
-@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
-    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
-  apply ext'
-  simp only [setIfInBounds]
-  split
-  · simp
-  · simp_all [List.set_eq_of_length_le]
-
 @[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'
@@ -2324,8 +2406,8 @@ abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
 
 @[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_is_setIfInBounds
 @[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
-@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_eq
-@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_eq
+@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_self
+@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_self
 @[deprecated getD_get?_setIfInBounds (since := "2024-11-24")] abbrev getD_setD := @getD_get?_setIfInBounds
 @[deprecated getElem_setIfInBounds (since := "2024-11-24")] abbrev getElem_setD := @getElem_setIfInBounds
 

src/Init/Data/BitVec/Lemmas.lean

@@ -241,8 +241,11 @@ theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
 @[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
   cases b <;> rfl
 
-@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
-  cases b <;> simp [BitVec.msb, getMsbD, getLsbD]
+@[simp] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by
+  cases b <;> rfl
+
+@[simp] theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat) := by
+  cases b <;> rfl
 
 theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  by
   rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']
@@ -366,6 +369,12 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
   · simp only [ofBool]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
+@[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by
+  cases b <;> simp [getMsbD]
+
+@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
+  cases b <;> simp [BitVec.msb]
+
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]

src/Init/Data/List/Lemmas.lean

@@ -253,6 +253,14 @@ theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) :
     l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
+theorem getD_getElem? (l : List α) (i : Nat) (d : α) :
+    l[i]?.getD d = if p : i < l.length then l[i]'p else d := by
+  if h : i < l.length then
+    simp [h, getElem?_def]
+  else
+    have p : i ≥ l.length := Nat.le_of_not_gt h
+    simp [getElem?_eq_none p, h]
+
 @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
 
 theorem getElem_cons {l : List α} (w : i < (a :: l).length) :

src/Init/Data/List/ToArray.lean

@@ -363,4 +363,12 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
+@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
+  apply ext'
+  simp only [setIfInBounds]
+  split
+  · simp
+  · simp_all [List.set_eq_of_length_le]
+
 end List

src/Lean/Elab/PreDefinition/Main.lean

@@ -22,7 +22,8 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa
       let value ← if useSorry then
         mkLambdaFVars xs (← mkSorry type (synthetic := true))
       else
-        liftM <| mkInhabitantFor preDef.declName xs type
+        let msg := m!"failed to compile 'partial' definition '{preDef.declName}'"
+        liftM <| mkInhabitantFor msg xs type
       addNonRec { preDef with
         kind  := DefKind.«opaque»
         value

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -50,13 +50,13 @@ private partial def mkInhabitantForAux? (xs insts : Array Expr) (type : Expr) (u
       return none
 
 /- TODO: add a global IO.Ref to let users customize/extend this procedure -/
-def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr :=
+def mkInhabitantFor (failedToMessage : MessageData) (xs : Array Expr) (type : Expr) : MetaM Expr :=
   withInhabitedInstances xs fun insts => do
     if let some val ← mkInhabitantForAux? xs insts type false <||> mkInhabitantForAux? xs insts type true then
       return val
     else
       throwError "\
-        failed to compile 'partial' definition '{declName}', could not prove that the type\
+        {failedToMessage}, could not prove that the type\
         {indentExpr (← mkForallFVars xs type)}\n\
         is nonempty.\n\
         \n\

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -20,6 +20,7 @@ structure EqnInfo extends EqnInfoCore where
   declNameNonRec  : Name
   fixedPrefixSize : Nat
   argsPacker      : ArgsPacker
+  hasInduct       : Bool
   deriving Inhabited
 
 private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
@@ -101,7 +102,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
-    (argsPacker : ArgsPacker) : MetaM Unit := do
+    (argsPacker : ArgsPacker) (hasInduct : Bool) : MetaM Unit := do
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-
   See issue #2327.
@@ -114,7 +115,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
           eqnInfoExt.insert env preDef.declName { preDef with
-            declNames, declNameNonRec, fixedPrefixSize, argsPacker }
+            declNames, declNameNonRec, fixedPrefixSize, argsPacker, hasInduct }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -178,7 +178,8 @@ def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Arr
     let type ← goal.getType
     let (.mdata _ (.app _ param)) := type
         | throwError "MVar does not look like a recursive call:{indentExpr type}"
-    let (funidx, _) ← argsPacker.unpack param
+    let some (funidx, _) := argsPacker.unpack param
+        | throwError "Cannot unpack param, unexpected expression:{indentExpr param}"
     r := r.modify funidx (·.push goal)
   return r
 

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -352,8 +352,10 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
         throwError "Insufficient arguments in recursive call"
       let arg := args[fixedPrefixSize]!
       trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
-      let (caller, params) ← argsPacker.unpack param
-      let (callee, args) ← argsPacker.unpack arg
+      let some (caller, params) := argsPacker.unpack param
+        | throwError "Cannot unpack param, unexpected expression:{indentExpr param}"
+      let some (callee, args) := argsPacker.unpack arg
+        | throwError "Cannot unpack arg, unexpected expression:{indentExpr arg}"
       RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args)
 
 /-- Is the expression a `<`-like comparison of `Nat` expressions -/
@@ -771,6 +773,8 @@ Main entry point of this module:
 
 Try to find a lexicographic ordering of the arguments for which the recursive definition
 terminates. See the module doc string for a high-level overview.
+
+The `preDefs` are used to determine arity and types of arguments; the bodies are ignored.
 -/
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
     (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -110,7 +110,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
     unless type.isForall do
       throwError "wfRecursion: expected unary function type: {type}"
     let packedArgType := type.bindingDomain!
-    elabWFRel preDefs unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
+    elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
@@ -142,7 +142,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
   let preDefs ← preDefs.mapM (abstractNestedProofs ·)
-  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
+  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker (hasInduct := true)
   for preDef in preDefs do
     markAsRecursive preDef.declName
     generateEagerEqns preDef.declName

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -51,12 +51,12 @@ If the `termArgs` map the packed argument `argType` to `β`, then this function
 continuation a value of type `WellFoundedRelation argType` that is derived from the instance
 for `WellFoundedRelation β` using `invImage`.
 -/
-def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (prefixArgs : Array Expr)
+def elabWFRel (declNames : Array Name) (unaryPreDefName : Name) (prefixArgs : Array Expr)
     (argsPacker : ArgsPacker) (argType : Expr) (termArgs : TerminationArguments)
     (k : Expr → TermElabM α) : TermElabM α := withDeclName unaryPreDefName do
   let α := argType
   let u ← getLevel α
-  let β ← checkCodomains (preDefs.map (·.declName)) prefixArgs argsPacker.arities termArgs
+  let β ← checkCodomains declNames prefixArgs argsPacker.arities termArgs
   let v ← getLevel β
   let packedF ← argsPacker.uncurryND (termArgs.map (·.fn.beta prefixArgs))
   let inst ← synthInstance (.app (.const ``WellFoundedRelation [v]) β)

src/Lean/Meta/ArgsPacker.lean

@@ -87,7 +87,7 @@ Unpacks a unary packed argument created with `Unary.pack`.
 
 Throws an error if the expression is not of that form.
 -/
-def unpack (arity : Nat) (e : Expr) : MetaM (Array Expr) := do
+def unpack (arity : Nat) (e : Expr) : Option (Array Expr) := do
   let mut e := e
   let mut args := #[]
   while args.size + 1 < arity do
@@ -95,11 +95,10 @@ def unpack (arity : Nat) (e : Expr) : MetaM (Array Expr) := do
       args := args.push (e.getArg! 2)
       e := e.getArg! 3
     else
-      throwError "Unexpected expression while unpacking n-ary argument"
+      none
   args := args.push e
   return args
 
-
 /--
   Given a (dependent) tuple `t` (using `PSigma`) of the given arity.
   Return an array containing its "elements".
@@ -258,7 +257,7 @@ argument and function index.
 
 Throws an error if the expression is not of that form.
 -/
-def unpack (numFuncs : Nat) (expr : Expr) : MetaM (Nat × Expr) := do
+def unpack (numFuncs : Nat) (expr : Expr) : Option (Nat × Expr) := do
   let mut funidx := 0
   let mut e := expr
   while funidx + 1 < numFuncs do
@@ -269,7 +268,7 @@ def unpack (numFuncs : Nat) (expr : Expr) : MetaM (Nat × Expr) := do
       e := e.getArg! 2
       break
     else
-      throwError "Unexpected expression while unpacking mutual argument:{indentExpr expr}"
+      none
   return (funidx, e)
 
 
@@ -377,14 +376,17 @@ and `(z : C) → R₂[z]`, returns an expression of type
 (x : A ⊕' C) → (match x with | .inl x => R₁[x] | .inr R₂[z])
 ```
 -/
-def uncurry (es : Array Expr) : MetaM Expr := do
-  let types ← es.mapM inferType
-  let resultType ← uncurryType types
+def uncurryWithType (resultType : Expr) (es : Array Expr) : MetaM Expr := do
   forallBoundedTelescope resultType (some 1) fun xs codomain => do
     let #[x] := xs | unreachable!
     let value ← casesOn x codomain es.toList
     mkLambdaFVars #[x] value
 
+def uncurry (es : Array Expr) : MetaM Expr := do
+  let types ← es.mapM inferType
+  let resultType ← uncurryType types
+  uncurryWithType resultType es
+
 /--
 Given unary expressions `e₁`, `e₂` with types `(x : A) → R`
 and `(z : C) → R`, returns an expression of type
@@ -414,7 +416,7 @@ def curryType (n : Nat) (type : Expr) : MetaM (Array Expr) := do
 
 end Mutual
 
--- Now for the main definitions in this moduleo
+-- Now for the main definitions in this module
 
 /-- The number of functions being packed -/
 def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size
@@ -422,6 +424,10 @@ def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size
 /-- The arities of the functions being packed -/
 def arities (argsPacker : ArgsPacker) : Array Nat := argsPacker.varNamess.map (·.size)
 
+def onlyOneUnary (argsPacker : ArgsPacker) :=
+  argsPacker.varNamess.size = 1 &&
+  argsPacker.varNamess[0]!.size = 1
+
 def pack (argsPacker : ArgsPacker) (domain : Expr) (fidx : Nat) (args : Array Expr)
     : MetaM Expr := do
   assert! fidx < argsPacker.numFuncs
@@ -436,14 +442,13 @@ return the function index that is called and the arguments individually.
 
 We expect precisely the expressions produced by `pack`, with manifest
 `PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
-rather than using projectinos.
+rather than using projections.
 -/
-def unpack (argsPacker : ArgsPacker) (e : Expr) : MetaM (Nat × Array Expr) := do
+def unpack (argsPacker : ArgsPacker) (e : Expr) : Option (Nat × Array Expr) := do
   let (funidx, e) ← Mutual.unpack argsPacker.numFuncs e
   let args ← Unary.unpack argsPacker.varNamess[funidx]!.size e
   return (funidx, args)
 
-
 /--
 Given types `(x : A) → (y : B[x]) → R₁[x,y]` and `(z : C) → R₂[z]`, returns the type uncurried type
 ```
@@ -465,6 +470,10 @@ def uncurry (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do
   let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
   Mutual.uncurry unary
 
+def uncurryWithType (argsPacker : ArgsPacker) (resultType : Expr) (es : Array Expr) : MetaM Expr := do
+  let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
+  Mutual.uncurryWithType resultType unary
+
 /--
 Given expressions `e₁`, `e₂` with types `(x : A) → (y : B[x]) → R`
 and `(z : C) → R`, returns an expression of type

src/Lean/Meta/Tactic/FunInd.lean

@@ -810,7 +810,8 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
       let args := e.getAppArgs
       if eqnInfo.fixedPrefixSize + 1 ≤ args.size then
         let packedArg := args.back!
-          let (i, unpackedArgs) ← eqnInfo.argsPacker.unpack packedArg
+          let some (i, unpackedArgs) := eqnInfo.argsPacker.unpack packedArg
+            | throwError "Unexpected packedArg:{indentExpr packedArg}"
           let e' := .const eqnInfo.declNames[i]! e.getAppFn.constLevels!
           let e' := mkAppN e' args.pop
           let e' := mkAppN e' unpackedArgs
@@ -1110,11 +1111,16 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false
   match s with
   | "induct" =>
-    if (WF.eqnInfoExt.find? env p).isSome then return true
+    if let some eqnInfo := WF.eqnInfoExt.find? env p then
+      unless eqnInfo.hasInduct do
+        return false
+      return true
     if (Structural.eqnInfoExt.find? env p).isSome then return true
     return false
   | "mutual_induct" =>
     if let some eqnInfo := WF.eqnInfoExt.find? env p then
+      unless eqnInfo.hasInduct do
+        return false
       if h : eqnInfo.declNames.size > 1 then
         return eqnInfo.declNames[0] = p
     if let some eqnInfo := Structural.eqnInfoExt.find? env p then

src/Lean/ResolveName.lean

@@ -398,16 +398,22 @@ Aliases are considered first.
 
 When `fullNames` is true, returns either `n₀` or `_root_.n₀`.
 
+When `allowHorizAliases` is false, then "horizontal aliases" (ones that are not put into a parent namespace) are filtered out.
+The assumption is that non-horizontal aliases are "API exports" (i.e., intentional exports that should be considered to be the new canonical name).
+"Non-API exports" arise from (1) using `export` to add names to a namespace for dot notation or (2) projects that want names to be conveniently and permanently accessible in their own namespaces.
+
 This function is meant to be used for pretty printing.
 If `n₀` is an accessible name, then the result will be an accessible name.
 -/
-def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) : m Name := do
+def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) (allowHorizAliases := false) : m Name := do
   if n₀.hasMacroScopes then return n₀
   if fullNames then
     match (← resolveGlobalName n₀) with
       | [(potentialMatch, _)] => if (privateToUserName? potentialMatch).getD potentialMatch == n₀ then return n₀ else return rootNamespace ++ n₀
       | _ => return n₀ -- if can't resolve, return the original
   let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
+  unless allowHorizAliases do
+    initialNames := initialNames.filter fun n => n.getPrefix.isPrefixOf n₀.getPrefix
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
     if let some n ← unresolveNameCore initialName then

tests/lean/run/5689.lean

@@ -0,0 +1,17 @@
+/-!
+# Pretty printing shouldn't make use of "non-API exports"
+-/
+
+namespace A
+def n : Nat := 22
+end A
+
+namespace B
+export A (n)
+end B
+
+/-!
+Was `B.n`
+-/
+/-- info: A.n : Nat -/
+#guard_msgs in #check (A.n)

tests/lean/run/DVec.lean

@@ -41,7 +41,7 @@ example (v : Vec Nat 1) : Nat :=
 -- Does not work: Aliases find that `v` could be the `TypeVec` argument since `TypeVec` is an abbrev for `Vec`.
 /--
 error: application type mismatch
-  @Vec.hd ?_ v
+  @DVec.hd ?_ v
 argument
   v
 has type

tests/lean/run/alias.lean

@@ -26,7 +26,7 @@ However, this dot notation fails since there is no `FinSet` argument.
 However, unfolding is the preferred method.
 -/
 /--
-error: invalid field notation, function 'FinSet.union' does not have argument with type (FinSet ...) that can be used, it must be explicit or implicit with a unique name
+error: invalid field notation, function 'Set.union' does not have argument with type (FinSet ...) that can be used, it must be explicit or implicit with a unique name
 -/
 #guard_msgs in
 example (x y : FinSet 10) : FinSet 10 :=