diff --git a/tests/lean/run/IO2.lean b/tests/lean/run/IO2.lean index a9f6d726a5..cc0dbc7331 100644 --- a/tests/lean/run/IO2.lean +++ b/tests/lean/run/IO2.lean @@ -6,8 +6,8 @@ open list since unit is at Type₁ -/ -definition for {A : Type} {B : Type} : list A → (A → IO B) → IO poly_unit +definition foreach {A : Type} {B : Type} : list A → (A → IO B) → IO poly_unit | [] f := return poly_unit.star -| (x::xs) f := do f x, for xs f +| (x::xs) f := do f x, foreach xs f -vm_eval for [1,2,3,4,5] (λ i, do put_str "value: ", put_nat i, put_str "\n") +vm_eval foreach [1,2,3,4,5] (λ i, do put_str "value: ", put_nat i, put_str "\n")