in lean/scripts/lint_style.py [0:0]
def import_only_check(lines, path):
import_only_file = True
errors = []
for line_nr, line in skip_comments(enumerate(lines, 1)):
imports = line.split()
if imports[0] == "--":
continue
if imports[0] != "import":
import_only_file = False
break
if len(imports) > 2:
if imports[2] == "--":
continue
else:
errors += [(ERR_IMP, line_nr, path)]
return (import_only_file, errors)