The .lean files adhere to the following guidelines: - A [[File header boilerplate|header section]] that includes author credits and a copyright notice that preserves any binding copyright conditions. The header section also includes a link the the LeanNotes web page that annotatates the .lean file. - [[Comment guidelines|Comments]] are typically pared with each line of code. A set of macros is used to streamline the uniform application of these comments. - [[LeanNote coding idioms]] are defined to help: - clarify the meaning of some tactics whose names tend to obscure their meaning. - lessen the need to glance back and forth between the code and the infoview. - [[Naming conventions]] are used to make the meaning of hypotheses easier to understand. - [[set_options]] enable a coding style that can be more appropriate for the beginning and intermediate Lean user. - Consistent formatting reduces "eye friction". This includes column alignment of similar lines of code and the inclusion of infoview information in comments that reduce the need to go back and forth between the code and infoview windows. Refer to the article [[Reducing eye friction]] --- Author: [[dducoff]] Posted Date: 2026-06-25