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