Timelib A date and time library for Lean 4, implementing the proleptic Gregorian calendar. See the file Timelib/NewDesign to see the new design, which accommodates timekeeping in any SI unit, using the SI power as a type index.