CMU Undergrad Course
Clone or download
Pull request Compare This branch is even with leanprover:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
_static
_templates
exclude
latex_images
png_images
.gitignore
LICENSE
Makefile
README.md
axiomatic_foundations.rst
bussproofs.sty
classical_reasoning.rst
combinatorics.rst
conf.py
deploy.sh
elementary_number_theory.rst
first_order_logic.rst
first_order_logic_in_lean.rst
functions.rst
functions_in_lean.rst
index.rst
introduction.rst
lean_sphinx.py
mylogic.sty
natural_deduction_for_first_order_logic.rst
natural_deduction_for_propositional_logic.rst
propositional_logic.rst
propositional_logic_in_lean.rst
relations.rst
relations_in_lean.rst
semantics_of_first_order_logic.rst
semantics_of_propositional_logic.rst
sets.rst
sets_in_lean.rst
the_infinite.rst
the_natural_numbers_and_induction.rst
the_natural_numbers_and_induction_in_lean.rst
the_real_numbers.rst
unixode.sty

README.md

Logic and Proof

Built using Sphinx and restructured text. Also requires convert (https://imagemagick.org) for image conversion.

How to build

The build requires python 3 (install python3-venv on ubuntu).

make install-deps
make images
make html
make latexpdf

The call to make install-deps is only required the first time, and only if you want to use the bundled version of Sphinx and Pygments with improved syntax highlighting for Lean.

The call to make images is also only required the first time, or if you add new latex source to latex_images after that.

How to test the Lean code snippets

make leantest

How to deploy

./deploy.sh leanprover logic_and_proof

How to contribute

Pull requests with corrections are welcome. Please follow our commit conventions <https://github.com/leanprover/lean/blob/master/doc/commit_convention.md>. If you have questions about whether a change will be considered helpful, please contact Jeremy Avigad, avigad@cmu.edu.