From 015c667eae0989a788ba8c3902175e080c78ed3e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Sep 2016 09:34:19 -0700 Subject: [PATCH] fix(tests/lean/run/IO2): bad overload --- tests/lean/run/IO2.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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")