max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: FunInd: omit unused parameters (#6330)

Browse source 
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
This commit is contained in:
Joachim Breitner 2024-12-07 02:57:00 +01:00
parent 279f36b4cc
commit 6447fda253
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Data/RArray.lean
View file

@ -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