coq-project
Diffusion coq-project (master)
Recent Commits
Recent Commits
Commit | Author | Details | Committed | ||||
---|---|---|---|---|---|---|---|
82a0cf06060d | • abgruszecki | Tweak the notebook | Dec 1 2021 | ||||
e618b5b97f63 | • abgruszecki | Fix escaping in README | Dec 1 2021 | ||||
a08ac82a3150 | • abgruszecki | Tweak the notebook further | Nov 30 2021 | ||||
f44ede4bf23d | • abgruszecki | Update the Coq workshop for 2021 | Nov 29 2021 | ||||
b3826dceb699 | • abgruszecki | Fix the definition of value | Nov 17 2020 | ||||
82508ce68c46 | • abgruszecki | Adjust advanced Coq notebook | Nov 17 2020 | ||||
6094ee76a6dd | • liufengyun/GitHub | Merge pull request #4 from lampepfl/rewrite-coq-intro | Nov 10 2020 | ||||
94fca067c934 | • abgruszecki | Adjust README.md | Nov 9 2020 | ||||
5bb567ac194a | • abgruszecki | Include 'Coq for POPL folk' as a notebook | Nov 9 2020 | ||||
dd6f828f3525 | • abgruszecki/GitHub | Merge pull request #3 from lampepfl/improve-2020 | Nov 9 2020 | ||||
e6b313e1483f | Liu Fengyun | Fix ordering of cells | Nov 4 2020 | ||||
9f9a0c19f973 | Liu Fengyun | Fix box type | Nov 4 2020 | ||||
f65134aee3cb | Liu Fengyun | Improve text and proof for even_double | Nov 4 2020 | ||||
b9bc924cb89b | Liu Fengyun | Fix typo | Dec 12 2019 | ||||
3ed179d31ada | liuf/GitHub | Merge pull request #2 from lampepfl/anatoliykmetyuk-patch-1 | Nov 21 2019 |
README.md
README.md
A Short Introduction to Coq
This is a repository with the Jupyter notebook used for the Coq workshop in the FoS course.
You can run these notebooks online, here are the links:
Running it locally
You will need to install Coq, Jupyter and the coq_jupyter kernel. You can do that more-or-less as follows:
shell brew install coq # or something similar for your OS pip install --user coq_jupyter==1.5.0 python -m coq_jupyter.install
Depending on your system, you may also need to run:
shell pip install --user notebook
Run
shell jupyter notebook
Note: using jupyter lab does not work correctly. Use the notebook version.
c4science · Help