My Lean playground for learning. By default, it won't work and will be wrong. Learn about Lean at https://leanprover.github.io A lot of code is copied from mathlib, the intention being that if I write it out myself line-by-line, I gain a better understanding of the process by which mathlib was created.
Some highlights:
kelley.leanis an experiment in formalising set/class theory within Lean.rb.leanis a port of Coq's RB trees implementation. I intend to add proofs, one day.docs/meta_*.mdis a tutorial I am writing on using themetafeatures of Lean.