commit: a91728075f5c34fb8c8e0575a05357012cd55fe3

[log]
author: Sofia Rodrigues <sofia@algebraic.dev>

Fri Jul 03 16:09:54 2026 -0300
committer: GitHub <noreply@github.com>

Fri Jul 03 19:09:54 2026 +0000
tree: 6bc16084d38742bd77c8305f45aed6430822b9fe
parent: 8f856a360656b71aca31a287a92f974176030eca [diff]

feat: add `RecurringRule` for `ZoneRules` for computing dates in the future (#13804)

This PR adds the parsing of Posix TZ String (generating a
`RecurringRule` type) in TzIf V2 and V3 footer so lean can generate
timezone transitions in case the timestamp is not covered by the
transitions array in `ZoneRules`.

src/Std/Time/Zoned/Database/Basic.lean[diff]
src/Std/Time/Zoned/Database/PosixTz.lean[Added - diff]
src/Std/Time/Zoned/RecurringRule.lean[Added - diff]
src/Std/Time/Zoned/ZoneRules.lean[diff]
tests/elab/timePosixTzFooter.lean[Added - diff]

5 files changed

tree: 6bc16084d38742bd77c8305f45aed6430822b9fe

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.