Commit 2020-05-01 10:09 ee488b27

fix(tactic/lint/basic): remove default argument for auto_decl and enable more linters (#2580) Run more linters on automatically-generated declarations. Quite a few linters should have been run on them, but I forgot about it because the auto_decls flag is optional and off by default. I've made it non-optional so that you don't forget about it when defining a linter. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20linter.20and.20structure.20fields/near/195810856