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

feat: add forIn'_eq_forIn theorem for lists

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-14 11:50:47 -07:00
parent 2ac9cfb7b1
commit cab3217b05
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Data/List/Control.lean
View file

@ -176,6 +176,15 @@ instance : ForIn m (List α) α where
instance : ForIn' m (List α) α inferInstance where
forIn' := List.forIn'
@[simp] theorem forIn'_eq_forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) : forIn' as init (fun a _ b => f a b) = forIn as init f := by
simp [forIn', forIn, List.forIn, List.forIn']
have : ∀ cs h, List.forIn'.loop cs (fun a x b => f a b) as init h = List.forIn.loop f as init := by
intro cs h
induction as generalizing cs init with
| nil => intros; rfl
| cons a as ih => intros; simp [List.forIn.loop, List.forIn'.loop, ih]
apply this
instance : ForM m (List α) α where
forM := List.forM