Part 1: Lean tips

The purpose of this part is to explain some non-mathematical details about Lean. The sections are independent of each other, and the primary use of this part is as a reference.

Contents:

• Types and terms
• Equality
• The three kinds of types
• Brackets in function inputs
• Notation and precedence
• Structures
• Classes
• Dot notation
• Coercions
• The axiom of choice
• How to format your code well