linter.fugue.autoImplicitOverride

autoImplicit is off project-wide (lakefile.lean). A per-file set_option autoImplicit true opts back in — never right; write every implicit explicitly. (The one-command set_option autoImplicit true in … form is peeled off before linters run and is not flagged.)