From 6447fda253a69b501d16641d2b7f5ff234c0e80e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 7 Dec 2024 02:57:00 +0100 Subject: [PATCH] feat: FunInd: omit unused parameters (#6330) This PR removes unnecessary parameters from the funcion induction principles. This is a breaking change; broken code can typically be adjusted simply by passing fewer parameters. Part 2, adjusting after stage0 update. Closes #6320 --- src/Lean/Data/RArray.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Data/RArray.lean b/src/Lean/Data/RArray.lean index c58f07fe10..54b7fd5612 100644 --- a/src/Lean/Data/RArray.lean +++ b/src/Lean/Data/RArray.lean @@ -35,7 +35,7 @@ theorem RArray.get_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) (i : Fin n) : go 0 n h (Nat.le_refl _) (Nat.zero_le _) i.2 where go lb ub h1 h2 (h3 : lb ≤ i.val) (h3 : i.val < ub) : (ofFn.go f lb ub h1 h2).get i = f i := by - induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n) + induction lb, ub, h1, h2 using RArray.ofFn.go.induct (n := n) case case1 => simp [ofFn.go, RArray.get_eq_getImpl, RArray.getImpl] congr @@ -53,7 +53,7 @@ theorem RArray.size_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) : go 0 n h (Nat.le_refl _) where go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by - induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n) + induction lb, ub, h1, h2 using RArray.ofFn.go.induct (n := n) case case1 => simp [ofFn.go, size]; omega case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega