private adaptions

Author: Kha

src/Init/Core.lean

@@ -95,7 +95,7 @@ structure Thunk (α : Type u) : Type u where
   -/
   mk ::
   /-- Extract the getter function out of a thunk. Use `Thunk.get` instead. -/
-  private fn : Unit → α
+  fn : Unit → α
 
 attribute [extern "lean_mk_thunk"] Thunk.mk
 

src/Init/Data/Array/Lemmas.lean

@@ -3707,7 +3707,7 @@ theorem back?_replicate {a : α} {n : Nat} :
 @[deprecated back?_replicate (since := "2025-03-18")]
 abbrev back?_mkArray := @back?_replicate
 
-@[simp] theorem back_replicate (w : 0 < n) : (replicate n a).back (by simpa using w) = a := by
+@[simp] theorem back_replicate {xs : Array α} (w : 0 < n) : (replicate n xs).back (by simpa using w) = xs := by
   simp [back_eq_getElem]
 
 @[deprecated back_replicate (since := "2025-03-18")]

src/Init/Data/Array/MapIdx.lean

@@ -413,7 +413,7 @@ theorem mapIdx_eq_mapIdx_iff {xs : Array α} :
   rcases xs with ⟨xs⟩
   simp [List.mapIdx_eq_mapIdx_iff]
 
-@[simp] theorem mapIdx_set {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} :
+@[simp] theorem mapIdx_set {f : Nat → α → β} {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} :
     (xs.set i a).mapIdx f = (xs.mapIdx f).set i (f i a) (by simpa) := by
   rcases xs with ⟨xs⟩
   simp [List.mapIdx_set]

src/Init/Data/Fin/Basic.lean

@@ -84,7 +84,7 @@ Examples:
  * `(2 : Fin 3) + (2 : Fin 3) = (1 : Fin 3)`
 -/
 protected def add : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, by exact mlt h⟩
 
 /--
 Multiplication modulo `n`, usually invoked via the `*` operator.
@@ -95,7 +95,7 @@ Examples:
  * `(3 : Fin 10) * (7 : Fin 10) = (1 : Fin 10)`
 -/
 protected def mul : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, by exact mlt h⟩
 
 /--
 Subtraction modulo `n`, usually invoked via the `-` operator.
@@ -122,7 +122,7 @@ protected def sub : Fin n → Fin n → Fin n
   using recursion on the second argument.
   See issue #4413.
   -/
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, by exact mlt h⟩
 
 /-!
 Remark: land/lor can be defined without using (% n), but
@@ -164,19 +164,19 @@ def modn : Fin n → Nat → Fin n
 Bitwise and.
 -/
 def land : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, by exact mlt h⟩
 
 /--
 Bitwise or.
 -/
 def lor : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, by exact mlt h⟩
 
 /--
 Bitwise xor (“exclusive or”).
 -/
 def xor : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.xor a b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.xor a b) % n, by exact mlt h⟩
 
 /--
 Bitwise left shift of bounded numbers, with wraparound on overflow.
@@ -187,7 +187,7 @@ Examples:
  * `(1 : Fin 10) <<< (4 : Fin 10) = (6 : Fin 10)`
 -/
 def shiftLeft : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a <<< b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a <<< b) % n, by exact mlt h⟩
 
 /--
 Bitwise right shift of bounded numbers.
@@ -201,7 +201,7 @@ Examples:
  * `(15 : Fin 17) >>> (2 : Fin 17) = (3 : Fin 17)`
 -/
 def shiftRight : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a >>> b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a >>> b) % n, by exact mlt h⟩
 
 instance : Add (Fin n) where
   add := Fin.add

src/Init/Data/Format/Basic.lean

@@ -294,7 +294,7 @@ private structure State where
   out    : String := ""
   column : Nat    := 0
 
-instance : MonadPrettyFormat (StateM State) where
+private instance : MonadPrettyFormat (StateM State) where
   -- We avoid a structure instance update, and write these functions using pattern matching because of issue #316
   pushOutput s       := modify fun ⟨out, col⟩ => ⟨out ++ s, col + s.length⟩
   pushNewline indent := modify fun ⟨out, _⟩ => ⟨out ++ "\n".pushn ' ' indent, indent⟩

src/Init/Data/Int/Basic.lean

@@ -269,7 +269,7 @@ set_option bootstrap.genMatcherCode false in
 
   Implemented by efficient native code. -/
 @[extern "lean_int_dec_nonneg"]
-private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
+def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
   match m with
   | ofNat m => isTrue <| NonNeg.mk m
   | -[_ +1] => isFalse <| fun h => nomatch h

src/Init/Data/Option/Basic.lean

@@ -437,9 +437,9 @@ This is the monadic analogue of `Option.getD`.
 @[simp, grind] theorem getDM_some [Pure m] (a : α) (y : m α) : (some a).getDM y = pure a := rfl
 
 instance (α) [BEq α] [ReflBEq α] : ReflBEq (Option α) where
-  rfl {x} :=
+  rfl {x} := by
     match x with
-    | some _ => BEq.rfl (α := α)
+    | some _ => exact BEq.rfl (α := α)
     | none => rfl
 
 instance (α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α) where

src/Init/Data/Repr.lean

@@ -210,7 +210,7 @@ protected def _root_.USize.repr (n : @& USize) : String :=
 private def reprArray : Array String := Id.run do
   List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
-private def reprFast (n : Nat) : String :=
+def reprFast (n : Nat) : String :=
   if h : n < Nat.reprArray.size then Nat.reprArray.getInternal n h else
   if h : n < USize.size then (USize.ofNatLT n h).repr
   else (toDigits 10 n).asString

src/Init/Data/Vector/Lemmas.lean

@@ -2968,7 +2968,7 @@ abbrev all_mkVector := @all_replicate
 section replace
 variable [BEq α]
 
-@[simp] theorem replace_cast {xs : Vector α n} {a b : α} :
+@[simp] theorem replace_cast {h : n = m} {xs : Vector α n} {a b : α} :
     (xs.cast h).replace a b = (xs.replace a b).cast (by simp [h]) := by
   rcases xs with ⟨xs, rfl⟩
   simp

src/Init/GetElem.lean

@@ -264,13 +264,13 @@ abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop
 /-! ### getElem? -/
 
 /-- Internal implementation of `as[i]?`. Do not use directly. -/
-private def get?Internal : (as : List α) → (i : Nat) → Option α
+def get?Internal : (as : List α) → (i : Nat) → Option α
   | a::_,  0   => some a
   | _::as, n+1 => get?Internal as n
   | _,     _   => none
 
 /-- Internal implementation of `as[i]!`. Do not use directly. -/
-private def get!Internal [Inhabited α] : (as : List α) → (i : Nat) → α
+def get!Internal [Inhabited α] : (as : List α) → (i : Nat) → α
   | a::_,  0   => a
   | _::as, n+1 => get!Internal as n
   | _,     _   => panic! "invalid index"

src/Init/Meta.lean

@@ -8,6 +8,7 @@ Additional goodies for writing macros
 module
 
 prelude
+import all Init.Prelude  -- for unfolding `Name.beq`
 import Init.MetaTypes
 import Init.Syntax
 import Init.Data.Array.GetLit
@@ -1190,7 +1191,7 @@ instance : Quote Nat numLitKind := ⟨fun n => Syntax.mkNumLit <| toString n⟩
 instance : Quote Substring := ⟨fun s => Syntax.mkCApp ``String.toSubstring' #[quote s.toString]⟩
 
 -- in contrast to `Name.toString`, we can, and want to be, precise here
-private def getEscapedNameParts? (acc : List String) : Name → Option (List String)
+def getEscapedNameParts? (acc : List String) : Name → Option (List String)
   | Name.anonymous => if acc.isEmpty then none else some acc
   | Name.str n s => do
     let s ← Name.escapePart s
@@ -1211,14 +1212,14 @@ instance [Quote α `term] [Quote β `term] : Quote (α × β) `term where
   quote
     | ⟨a, b⟩ => Syntax.mkCApp ``Prod.mk #[quote a, quote b]
 
-private def quoteList [Quote α `term] : List α → Term
+def quoteList [Quote α `term] : List α → Term
   | []      => mkCIdent ``List.nil
   | (x::xs) => Syntax.mkCApp ``List.cons #[quote x, quoteList xs]
 
 instance [Quote α `term] : Quote (List α) `term where
   quote := quoteList
 
-private def quoteArray [Quote α `term] (xs : Array α) : Term :=
+def quoteArray [Quote α `term] (xs : Array α) : Term :=
   if xs.size <= 8 then
     go 0 #[]
   else

src/Init/Prelude.lean

@@ -2459,7 +2459,7 @@ structure Char where
   /-- The value must be a legal scalar value. -/
   valid : val.isValidChar
 
-private theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size :=
+theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size :=
   match h with
   | Or.inl h      => Nat.lt_trans h (of_decide_eq_true rfl)
   | Or.inr ⟨_, h⟩ => Nat.lt_trans h (of_decide_eq_true rfl)
@@ -4060,8 +4060,13 @@ protected opaque String.hash (s : @& String) : UInt64
 instance : Hashable String where
   hash := String.hash
 
+end  -- don't expose `Lean` defs
+
 namespace Lean
 
+open BEq (beq)
+open HAdd (hAdd)
+
 /--
 Hierarchical names consist of a sequence of components, each of
 which is either a string or numeric, that are written separated by dots (`.`).
@@ -4146,35 +4151,35 @@ abbrev mkSimple (s : String) : Name :=
   .str .anonymous s
 
 /-- Make name `s₁` -/
-@[reducible] def mkStr1 (s₁ : String) : Name :=
+@[expose, reducible] def mkStr1 (s₁ : String) : Name :=
   .str .anonymous s₁
 
 /-- Make name `s₁.s₂` -/
-@[reducible] def mkStr2 (s₁ s₂ : String) : Name :=
+@[expose, reducible] def mkStr2 (s₁ s₂ : String) : Name :=
   .str (.str .anonymous s₁) s₂
 
 /-- Make name `s₁.s₂.s₃` -/
-@[reducible] def mkStr3 (s₁ s₂ s₃ : String) : Name :=
+@[expose, reducible] def mkStr3 (s₁ s₂ s₃ : String) : Name :=
   .str (.str (.str .anonymous s₁) s₂) s₃
 
 /-- Make name `s₁.s₂.s₃.s₄` -/
-@[reducible] def mkStr4 (s₁ s₂ s₃ s₄ : String) : Name :=
+@[expose, reducible] def mkStr4 (s₁ s₂ s₃ s₄ : String) : Name :=
   .str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄
 
 /-- Make name `s₁.s₂.s₃.s₄.s₅` -/
-@[reducible] def mkStr5 (s₁ s₂ s₃ s₄ s₅ : String) : Name :=
+@[expose, reducible] def mkStr5 (s₁ s₂ s₃ s₄ s₅ : String) : Name :=
   .str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅
 
 /-- Make name `s₁.s₂.s₃.s₄.s₅.s₆` -/
-@[reducible] def mkStr6 (s₁ s₂ s₃ s₄ s₅ s₆ : String) : Name :=
+@[expose, reducible] def mkStr6 (s₁ s₂ s₃ s₄ s₅ s₆ : String) : Name :=
   .str (.str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅) s₆
 
 /-- Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇` -/
-@[reducible] def mkStr7 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ : String) : Name :=
+@[expose, reducible] def mkStr7 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ : String) : Name :=
   .str (.str (.str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅) s₆) s₇
 
 /-- Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇.s₈` -/
-@[reducible] def mkStr8 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ : String) : Name :=
+@[expose, reducible] def mkStr8 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ : String) : Name :=
   .str (.str (.str (.str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅) s₆) s₇) s₈
 
 /-- (Boolean) equality comparator for names. -/
@@ -4423,7 +4428,7 @@ def Syntax.node8 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ a
 Singleton `SyntaxNodeKinds` are extremely common. They are written as name literals, rather than as
 lists; list syntax is required only for empty or non-singleton sets of kinds.
 -/
-def SyntaxNodeKinds := List SyntaxNodeKind
+@[expose] def SyntaxNodeKinds := List SyntaxNodeKind
 
 /--
 Typed syntax, which tracks the potential kinds of the `Syntax` it contains.
@@ -5110,7 +5115,8 @@ namespace Macro
 /-- References -/
 private opaque MethodsRefPointed : NonemptyType.{0}
 
-private def MethodsRef : Type := MethodsRefPointed.type
+/-- An opaque reference to the `Methods` object. -/
+def MethodsRef : Type := MethodsRefPointed.type
 
 private instance : Nonempty MethodsRef := MethodsRefPointed.property
 

src/Init/Util.lean

@@ -32,13 +32,13 @@ def dbgStackTrace {α : Type u} (f : Unit → α) : α := f ()
 @[extern "lean_dbg_sleep"]
 def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
 
-@[noinline] private def mkPanicMessage (modName : String) (line col : Nat) (msg : String) : String :=
+@[noinline] def mkPanicMessage (modName : String) (line col : Nat) (msg : String) : String :=
   "PANIC at " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
 
 @[never_extract, inline, expose] def panicWithPos {α : Sort u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=
   panic (mkPanicMessage modName line col msg)
 
-@[noinline, expose] private def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
+@[noinline, expose] def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
   "PANIC at " ++ declName ++ " " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
 
 @[never_extract, inline, expose] def panicWithPosWithDecl {α : Sort u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α :=

src/Init/WF.lean

@@ -157,14 +157,8 @@ end Subrelation
 namespace InvImage
 variable {α : Sort u} {β : Sort v} {r : β → β → Prop}
 
-private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x := by
-  induction ac with
-  | intro x acx ih =>
-    intro z e
-    apply Acc.intro
-    intro y lt
-    subst x
-    apply ih (f y) lt y rfl
+def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x :=
+  Acc.recOn ac fun _ _ ih => fun _ e => Acc.intro _ (fun y lt => ih (f y) (e ▸ lt) y rfl)
 
 -- `def` for `WellFounded.fix`
 def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=