diff --git a/tests/lean/error_full_names.lean b/tests/lean/error_full_names.lean index 7f9aebd186..77ea016526 100644 --- a/tests/lean/error_full_names.lean +++ b/tests/lean/error_full_names.lean @@ -1,4 +1,4 @@ -import data.nat +import data.nat.basic namespace foo open nat inductive nat : Type := zero, foosucc : nat → nat