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) #[]"