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

chore: restore @[simp] to List.ofFn_succ (#8427)

Browse source
This commit is contained in:
Kim Morrison 2025-05-21 13:12:26 +10:00 • committed by GitHub
parent c28b052576
commit 79254d039c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Data/List/OfFn.lean
View file

@ -71,6 +71,7 @@ protected theorem getElem?_ofFn {f : Fin n → α} :
theorem ofFn_zero {f : Fin 0 → α} : ofFn f = [] := by
rw [ofFn, Fin.foldr_zero]
@[simp]
theorem ofFn_succ {n} {f : Fin (n + 1) → α} : ofFn f = f 0 :: ofFn fun i => f i.succ :=
ext_get (by simp) (fun i hi₁ hi₂ => by
cases i
@ -91,7 +92,7 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
ofFn f = (ofFn fun i => f (i.castLE (Nat.le_add_right n m))) ++ (ofFn fun i => f (i.natAdd n)) := by
induction m with
| zero => simp
| succ m ih => simp [ofFn_succ_last, ih]
| succ m ih => simp [-ofFn_succ, ofFn_succ_last, ih]
@[simp]
theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
@ -175,6 +176,6 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
unfold Id.run
induction n with
| zero => simp
| succ n ih => simp [ofFnM_succ_last, ofFn_succ_last, ih]
| succ n ih => simp [-ofFn_succ, ofFnM_succ_last, ofFn_succ_last, ih]
end List