95dbac26cf
This PR reduces the import closure of `Std.Time` such that it doesn't have to be rebuilt on every change in `Init.Data`. Noticed while working on `Init` refactorings. |
||
|---|---|---|
| .. | ||
| Date | ||
| DateTime | ||
| Format | ||
| Internal | ||
| Notation | ||
| Time | ||
| Zoned | ||
| Date.lean | ||
| DateTime.lean | ||
| Duration.lean | ||
| Format.lean | ||
| Internal.lean | ||
| Notation.lean | ||
| Time.lean | ||
| Zoned.lean | ||