Theorem Proving in Lean
=======================

.. toctree::
    :numbered:
    :maxdepth: 2

    introduction
    dependent_type_theory
    propositions_and_proofs
    quantifiers_and_equality
    tactics
    interacting_with_lean
    inductive_types
    induction_and_recursion
    structures_and_records
    type_classes
    axioms_and_computation

.. Indices and tables
   ==================
   * :ref:`genindex`
   * :ref:`modindex`
   * :ref:`search`