Markus Himmel

Hi, for PRs that build on other PRs, we usually have the later PR (in your case, this one) also have `master` as the target branch, but record the dependency...

> I guess we have homology and exactness now, right? The definitions are there, yes, though I would say that the API for both is not yet in a shape...

> Could we have a constructor `TreeMap \to ExtTreeMap`? In https://github.com/leanprover/lean4/pull/8004#discussion_r2056101702 we decided to do all of the "connect the map variants" functions at a later date with a structured...

Okay, I have moved the classes to Init.

I think it would already help if the box contained something high-level like like "Creating new Lean project" or "Busy creating new Lean project" in front of "Updating dependencies".

> However, I think that it is important to keep the support for leap seconds just to try keep the support for ISO 8601 compliant dates. If I'm understanding you...

I think the missing `DateTime` functions indicated in the Google sheet are still missing.

You removed the test that called `defaultGetLocalZoneRules`, but I think the failing test actually highlighted a real issue that I can reproduce when setting time zone on my computer to...

Hi @eric-wieser, thank you for taking the time to read through the PR. Our current priorities are to get the public API right and to get the PR merged. As...

> I don't agree, the `Mul` instance for `Minutes.Offset` is derived later Thanks, I had missed this. I agree that the `Offset` types should not derive `Mul` or `Div`. We...