diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index ddb0ad5bc8..11c2d75ece 100644 --- a/tests/lean/run/frontend1.lean +++ b/tests/lean/run/frontend1.lean @@ -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"