.. Mathematics in Lean documentation master file
   
Lean by example
===============

A guide for mathematicians who want to learn how to check their proofs on a computer. Suitable for mathematics undergraduates.

Introduction
------------

.. toctree::
   :maxdepth: 1

   introduction/introduction

Exercises
---------

.. toctree::
   :maxdepth: 1

	   
   
Tactic guide
------------

.. toctree::

   tactics/guide.rst

Appendix : dependent type theory.
---------------------------------

.. toctree::
   :maxdepth: 1

   appendix/type_theory
   appendix/functions
   appendix/inductive_types

Indices and tables
==================

* :ref:`genindex`
* :ref:`modindex`
* :ref:`search`