Part B: 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.

.. toctree::
   :maxdepth: 1
   :caption: Contents:


   typesandterms
   equality
   threekindsoftypes
   brackets
   structures
   classes
   dot_notation
   coercions