From 3e5527219fb5602f8a04aaec06cfe075860fd344 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Dec 2019 12:05:45 -0800 Subject: [PATCH] test: add foldl test --- tests/lean/run/frontend1.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index cc5bb131b9..aa7f9bd946 100644 --- a/tests/lean/run/frontend1.lean +++ b/tests/lean/run/frontend1.lean @@ -147,7 +147,8 @@ f a -- #check fun x => foo x x.w s4 -- fails in old elaborator -- #check bla (fun x => x.w) s4 -- fails in the old elaborator +-- #check #[1, 2, 3].foldl (fun r a => r.push a) #[] -- fails in the old elaborator #eval run "#check fun x => foo x x.w s4" #eval run "#check bla (fun x => x.w) s4" -#eval run "#check #[1, 2, 3]" +#eval run "#check #[1, 2, 3].foldl (fun r a => r.push a) #[]"