chore: make internal List getters private

2026-04-22 20:14:08 +00:00 · 2025-02-18 14:06:50 +11:00
1 changed files with 3 additions and 3 deletions
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -247,16 +247,16 @@ theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.leng
@[deprecated getElem_cons_drop_succ_eq_drop (since := "2024-11-05")]
 abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop

-/-! ### getElem?-/
+/-! ### getElem? -/

 /-- Internal implementation of `as[i]?`. Do not use directly. -/
-def get?Internal : (as : List α) → (i : Nat) → Option α
+private 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. -/
-def get!Internal [Inhabited α] : (as : List α) → (i : Nat) → α
+private def get!Internal [Inhabited α] : (as : List α) → (i : Nat) → α
  | a::_,  0   => a
  | _::as, n+1 => get!Internal as n
  | _,     _   => panic! "invalid index"