/edlib

Some personal experiments in Lean

Primary LanguageLean

Edlib

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.lean is an experiment in formalising set/class theory within Lean.
  • rb.lean is a port of Coq's RB trees implementation. I intend to add proofs, one day.
  • docs/meta_*.md is a tutorial I am writing on using the meta features of Lean.