This library is deprecated in favor of a version compatible with Lean4. Please see the new repository here Documentation and comments in this repository may be out of date with both the code here and with new versions of the library in Lean4.