- [[set_options]] enable a coding style that can be more appropriate for the beginning and intermediate Lean user. Depending on the .lean file, one or more of these options may be appropriate: | Set options | Description | | ------------------------------------------ | ----------------------------------------------------------------------- | | set_option eval.type true | Include the expression type when an \#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 | --- Author: [[dducoff]] Posted Date: 2026-06-25