max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: add foldl test

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-19 12:05:45 -08:00
parent ea2cebaf74
commit 3e5527219f
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/run/frontend1.lean
View file

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