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

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

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