A place to collect things I learn about Coq.
Fun things I've done so far:
- Equivalence between two definitions of a well-founded relation (Coq's and Wikipedia's) using classical logic (my proof)
- Formalization of the simply typed lambda calculus (following TaPL)