This project is an implementation of the Brown Benchmark for Table Types (B2T2) in Lean 4. Further documentation is forthcoming; in the meantime, refer to the B2T2 API specification.

Note: because this project began at a time when much of Mathlib had yet to be ported to Lean 4, this project does not depend on Mathlib and is entirely self-contained. Many of its definitions have likely since been added to Mathlib, which may cause conflicts.