diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index 09b56820d5..e279471fe7 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -27,9 +27,11 @@ set_option pp.all true #check foo 1 -#check foo 3 (c := Bool.false) +#check foo 3 (c := false) def Nat.boo (a : Nat) := succ a -- succ here is resolved as `Nat.succ`. #check Nat.boo + +#check true