Theorem: Array.foldr_step (GMLInit/Data/Array/Basic.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ foldr f b as (start + 1) stop = foldr f (f as[start] b) as start stop
Tactic:
apply foldrM_step
State after:
case hstop
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ stop ≤ start

State before:
case hstop
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ stop ≤ start
Tactic:
assumption
State after:
no goals