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

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

case hstop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ stop ≤ as.size

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

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

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