Timelib

A date and time library for Lean 4, implementing the proleptic Gregorian calendar.

Documentation

To generate timelib's documentation, first update in dev mode as doc-gen4 is an optional dependency.

> lake -R -Kenv=dev update

Then actually generate the documentation with

> lake -R -Kenv=dev build Timelib:docs

Almost done, the HTML is in .lake/build/doc, but accessing it via a browser requires an HTTP server. For instance, using python's http.server:

> python3 -m http.server -d .lake/build/doc