Commit 2024-05-24 03:47 f966474a

View on Github →

feat: syntax linter for #-commands (#11019) A Lean-linter implementation of the #-command linter introduced in #10809. This linter produces a warning whenever a non-allowed #-command is used. The allowed commands are

#align
#align_import
#noalign
#adaptation_note

Zulip discussion

Estimated changes