Commit 2024-06-19 08:39 60fd11f2
View on Github →feat: rewrite set_option style linter in lean (#12928) Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.
feat: rewrite set_option style linter in lean (#12928) Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.