Changelog

leanprover/lean4 · · 4 commits

Lean adds mergeSort lemmas and quieter termination hints

New mergeSort lemmas and an opt-out for redundant termination warnings headline the day; a couple docs/process nits round it out.

kim-em Rob23oba ia0

Add mergeSort lemmas for balanced splits and pairs (kim-em6778cc8)

Lean now exposes mergeSort_append and mergeSort_pair, giving direct lemmas for sorting a list built from a balanced split and for the 2-element case. This makes List.mergeSort easier to use without depending on internal split machinery, and the pair lemma is marked @[simp] for convenience.

Allow suppressing redundant termination warnings (Rob23oba19c7959)

TerminationHints gains a warnIfRedundant flag, and TerminationHints.ensureNone now skips emitting warnings when it is set to false. That matters for generated pre-definitions via addPreDefinitions, where redundant hints can be intentional and noisy warnings would otherwise get in the way.

Other misc changes

  • Doc typo fix in the List.lex example (c632a0a)
  • CLAUDE.md update to forbid process narrative in PR descriptions (3facd36)