- [[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 | | `set_option autoImplicit false` | <br> With this option off, you must explicitly declare all implicit arguments. This can be useful for debugging or for writing very precise, low-level definitions.<br> | | `set_option trace.Meta.Tactic.dsimp true` | [Lean4: explain set_option trace.Meta.Tactic.dsimp true - Google Search](https://www.google.com/search?client=safari&rls=en&q=Lean4%3A+explain+set_option+trace.Meta.Tactic.dsimp+true&ie=UTF-8&oe=UTF-8)<br>Display in the infoview or the message log the steps when the dsimp tactic is evaluated [[1](https://lean-lang.org/doc/reference/latest/The-Simplifier/Configuring-Simplification/), [2](https://lean-lang.org/doc/reference/latest/releases/v4.12.0/), [3](https://github.com/leanprover/lean4/issues/6969), [4](https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/)] | --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date:`** 2026-08-18