case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ fillNones as as' = fillNonesTR as as'
⊢ @fillNones = @fillNonesTR
funext α as as'
case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ fillNones as as' = fillNonesTR.go as as' #[]
case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ fillNones as as' = fillNonesTR as as'
simp [fillNonesTR]
case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ fillNones as as' = fillNonesTR.go as as' #[]
case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ fillNones as as' = fillNonesTR.go as as' #[]
let rec go (acc) : ∀ as as', @fillNonesTR.go α as as' acc = acc.data ++ as.fillNones as'
| [], _ => by simp [fillNonesTR.go]
| some a :: as, as' => by simp [fillNonesTR.go, go _ as as']
| none :: as, [] => by simp [fillNonesTR.go, reduceOption, filterMap_eq_filterMapTR.go]
| none :: as, a :: as' => by simp [fillNonesTR.go, go _ as as']
no goals
case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ fillNones as as' = fillNonesTR.go as as' #[]
simp [fillNonesTR, go]
no goals
α : Type u_1
as : List (Option α)
as' : List α
acc : Array α
x✝ : List α
⊢ fillNonesTR.go [] x✝ acc = acc.data ++ fillNones [] x✝
simp [fillNonesTR.go]
no goals
α : Type u_1
as✝ : List (Option α)
as'✝ : List α
acc : Array α
a : α
as : List (Option α)
as' : List α
⊢ fillNonesTR.go (some a :: as) as' acc = acc.data ++ fillNones (some a :: as) as'
simp [fillNonesTR.go, go _ as as']
no goals
α : Type u_1
as✝ : List (Option α)
as' : List α
acc : Array α
as : List (Option α)
⊢ fillNonesTR.go (none :: as) [] acc = acc.data ++ fillNones (none :: as) []
simp [fillNonesTR.go, reduceOption, filterMap_eq_filterMapTR.go]
no goals
α : Type u_1
as✝ : List (Option α)
as'✝ : List α
acc : Array α
as : List (Option α)
a : α
as' : List α
⊢ fillNonesTR.go (none :: as) (a :: as') acc = acc.data ++ fillNones (none :: as) (a :: as')
simp [fillNonesTR.go, go _ as as']