Skip to content

Instantly share code, notes, and snippets.

Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@juanbelieni
juanbelieni / MonadicParsing.lean
Created December 31, 2023 19:14
Monadic parsing in Lean
/-
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
@juanbelieni
juanbelieni / Peano.lean
Last active January 6, 2024 12:33
Peano numbers in Lean
/-
# 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
juanbelieni / Dockerfile
Last active March 11, 2021 15:34
Docker configuration for Anaconda and Jupyter Notebook
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=''"]