This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /- | |
| Implementation of monadic parsing in Lean, based on the original | |
| paper's implementation in Haskell. | |
| - FUNCTIONAL PEARL - Monadic parsing in Haskell: | |
| https://www.cmi.ac.in/~spsuresh/teaching/prgh15/papers/monadic-parsing.pdf | |
| -/ | |
| -- ## Parser definition |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /- | |
| # Peano numbers in Lean | |
| Proof that the set of natural numbers under ordinary addition and multiplication | |
| is a commutative semiring using the Peano numbers. | |
| - Peano axioms - Wikipedia: https://en.wikipedia.org/wiki/Peano_axioms | |
| - Semiring - Wikipedia: https://en.wikipedia.org/wiki/Semiring | |
| - Proofs involving the addition of natural numbers - Wikipedia: | |
| https://en.wikipedia.org/wiki/Proofs_involving_the_addition_of_natural_numbers |
juanbelieni
/ Dockerfile
Last active
March 11, 2021 15:34
Docker configuration for Anaconda and Jupyter Notebook
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| FROM continuumio/anaconda3:latest | |
| RUN conda install jupyter -y --quiet | |
| RUN mkdir /opt/notebooks | |
| CMD ["jupyter", "notebook", "--notebook-dir=/opt/notebooks", "--ip='*'", "--port=8888", "--no-browser", "--allow-root", "--NotebookApp.token=''", "--NotebookApp.password=''"] |