diff --git a/tests/lean/noTabs.lean b/tests/lean/noTabs.lean new file mode 100644 index 0000000000..9475259eba --- /dev/null +++ b/tests/lean/noTabs.lean @@ -0,0 +1,4 @@ +#check + let a := 1 + let b := 2 + a + b diff --git a/tests/lean/noTabs.lean.expected.out b/tests/lean/noTabs.lean.expected.out new file mode 100644 index 0000000000..6037902e5c --- /dev/null +++ b/tests/lean/noTabs.lean.expected.out @@ -0,0 +1 @@ +noTabs.lean:3:0: error: tabs are not allowed; please configure your editor to expand them