.. Lean Reference Manual documentation master file, created by sphinx-quickstart on Mon Jul 17 21:46:05 2017. You can adapt this file completely to your liking, but it should at least contain the root `toctree` directive. The Lean Reference Manual ========================= .. toctree:: :numbered: :maxdepth: 2 using_lean lexical_structure expressions declarations other_commands tactics programming metaprogramming libraries