logic_and_proof
logic_and_proof copied to clipboard
leanprover
CMU Undergrad Course
Current text: "In the Prior Analytics, the ancient Greek philosopher set out to analyze patterns of reasoning, and developed the theory of the syllogism." Corrected text: "In the Prior Analytics,...
The Fix for this actually comes from Kyle Miller (https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Joel.20McCracken/near/328720514)
I merely tested that the build succeeded, but haven't gone over the output yet. About the change to `sphinx.directives.CodeBlock`, we can see in the following commit that it appears to...
make files in two ways: 1. `make install-deps` fails because https://bitbucket.org/gebner/pygments-main/get/default.tar.gz#egg=Pygments does not exist. I replaced this with just `pip install pygments`. 2. `make html` fails for a reason I...
https://github.com/leanprover/logic_and_proof/blob/master/natural_deduction_for_propositional_logic.rst#L432 "or from applying the **or-elimination** rule to C and C → A" - is it supposed to be "or from applying the **implication-elimination** rule to C and C →...
I got many error like ``` writing output... [100%] venv/lib/python3.7/site-packages/sphinx/ext/autosummary/templates/autosummary/module /Users/ar/work/logic_and_proof/classical_reasoning.rst:237: WARNING: Could not lex literal_block as "lean". Highlighting skipped. /Users/ar/work/logic_and_proof/classical_reasoning.rst:378: WARNING: Could not lex literal_block as "lean". Highlighting skipped....
