Every Lean file is a sequence of toplevel declarations. These are the building blocks of every program and proof. This appendix provides a quick reference for all declaration types, with links to detailed explanations in the main text.
The distinction between def and theorem matters for performance. Lean marks theorem proofs as opaque, meaning they are never unfolded during type checking. This keeps proof terms from bloating computations. Use def for values you need to compute with and theorem for propositions you need to prove.
These commands are prefixed with # to distinguish them from regular declarations. They produce output but do not contribute to the compiled program. Use them liberally during development to inspect types and evaluate expressions.