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

chore: fix name of new Fin.foldlM_eq_finRange_foldlM lemmas (#8425)

Browse source
This commit is contained in:
Kim Morrison 2025-05-21 10:30:33 +10:00 • committed by GitHub
parent a9a069a0ef
commit a541b8e75e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Array/OfFn.lean
View file

@ -82,7 +82,7 @@ theorem ofFnM_succ' {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
let a ← f 0
let as ← ofFnM fun i => f i.succ
pure (#[a] ++ as)) := by
simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.foldlM_push_eq_append, List.finRange_succ, Function.comp_def]
simp [ofFnM, Fin.foldlM_eq_foldlM_finRange, List.foldlM_push_eq_append, List.finRange_succ, Function.comp_def]
theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
ofFnM f = (do

6
src/Init/Data/List/FinRange.lean
View file

@ -61,7 +61,7 @@ end List
namespace Fin
theorem foldlM_eq_finRange_foldlM [Monad m] (f : α → Fin n → m α) (x : α) :
theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x : α) :
foldlM n f x = (List.finRange n).foldlM f x := by
induction n generalizing x with
| zero => simp
@ -71,7 +71,7 @@ theorem foldlM_eq_finRange_foldlM [Monad m] (f : α → Fin n → m α) (x : α)
funext y
simp [ih, List.foldlM_map]
theorem foldrM_eq_finRange_foldrM [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
theorem foldrM_eq_foldrM_finRange [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
foldrM n f x = (List.finRange n).foldrM f x := by
induction n generalizing x with
| zero => simp
@ -101,7 +101,7 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
let a ← f 0
let as ← ofFnM fun i => f i.succ
pure (a :: as)) := by
simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.finRange_succ, List.foldlM_cons_eq_append,
simp [ofFnM, Fin.foldlM_eq_foldlM_finRange, List.finRange_succ, List.foldlM_cons_eq_append,
List.foldlM_map]
end List