chore: fix test

This commit is contained in:
Leonardo de Moura 2020-01-11 13:55:31 -08:00
parent 6762f8ea9a
commit f83678f19b

View file

@ -61,7 +61,7 @@ pure "hello"
#check (α : Type) → αα
#check {α : Type} → {β : Type} → M → (α → β) → α → β
#check ()
#check run
#check _root_.run
end"
structure S1 :=
@ -158,7 +158,6 @@ f a
#eval run "#check #[1, 2].foldl (fun r a => r.push a $.push a $.push a) #[]"
#eval run "#check #[1, 2].foldl (init := #[]) $ fun r a => r.push a $.push a"
#eval run "#check let x := one + zero; x + x"
-- set_option trace.Elab true
#eval run "#check (fun x => let v := x.w; v + v) s4"