Depending on the .lean file, one or more of these options may be appropriate: - `set_option eval.type true`-- include the expression type when \#eval expression is computed. - `set_option linter.style.emptyLine false` -- disable blank line warning inside a definition. - `set_option autoImplicit false` -- Disallow implicit arguments so that everything is explicitly declared. - `set_option linter.style.commandStart false` -- disable warnings for columnized spacing - `set_option linter.style.whitespace false` -- ignore whitespace errors, including alignment spacing