lean4-htt/RELEASES.md

v4.0.0-m4

• Support notation let <pattern> := <expr> | <else-case> in do blocks.

• Remove support for "auto" pure. In the Zulip thread, the consensus seemed to be that "auto" pure is more confusing than its worth.

• Remove restriction in congr theorems that all function arguments on the left-hand-side must be free variables. For example, the following theorem is now a valid congr theorem.

@[congr]
theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] :
                  ∀ {i j} (h : i = j) (x : p i) (y : α) (hx : x = y), Pi.single (f := (p ·)) i x = Pi.single (f := (p ·)) j ⟨y, hx ▸ h ▸ x.2⟩ :=

• Partially applied congruence theorems.

• Improve elaboration postponement heuristic when expected type is a metavariable. Lean now reduces the expected type before performing the test.