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

State before:
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldl f b as stop stop = b
Tactic:
apply foldlM_stop
State after:
case hstop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ stop ≤ as.size

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