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. - [[LeanNotes coding idioms|Code idioms]] are defined to help clarify the meaning of some tactics whose names tend to obscure their meaning. Idiom rules also help lesson 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. - Certain [[set_options]] enable a coding style that is more appropriate for the beginning Lean user.c - Consistent formatting that 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]]