Theorem Proving in Lean 3 (outdated)

.. 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