in lean/scripts/lint_style.py [0:0]
def skip_comments(enumerate_lines):
in_comment = False
for line_nr, line in enumerate_lines:
if "/-" in line:
in_comment = True
if "-/" in line:
in_comment = False
continue
if line == "\n" or in_comment:
continue
yield line_nr, line