nightly-2024-03-28

Changes since nightly-2024-03-27:

• Added @[induction_eliminator] and @[cases_eliminator] attributes to be able to define custom eliminators
  for the induction and cases tactics, replacing the @[eliminator] attribute.
  Gives custom eliminators for Nat so that induction and cases put goal states into terms of 0 and n + 1
  rather than Nat.zero and Nat.succ n.
  Added option tactic.customEliminators to control whether to use custom eliminators.
  #3629 and
  #3655.

Full commit log

• 55b7b07 feat: lake: alternative TOML config (#3298)
• 0963f34 chore: extend GetElem with getElem! and getElem? (#3694)
• 7989f62 fix: remove unused try catch (#3794)
• 4bacd70 feat: add option tactic.customEliminators to be able to turn off custom eliminators for induction and cases (#3655)
• 775dabd fix: toUInt64LE! and toUInt64BE! are swapped (#3660)
• 5167324 doc: edit Lean.MVarId.withReverted (#3743)
• 520cd3f fix: make generalized field notation for abbreviation types handle optional parameters (#3746)
• 5b7ec44 chore: fix rebase suggestion for Mathlib CI (#3701)
• 70924be feat: hovering over omission term shows reason for omission (#3751)
• 02c5700 feat: change apply_rfl tactic so that it does not operate on = (#3784)
• 3ee1cdf chore: CI: continue on test-summary failure
• 94d6286 chore: reorganising to reduce imports (#3790)
• 16fdca1 chore: test results as job summary (#3715)
• c857d08 fix: remove derive_functional_induction (#3788)
• 1a5d064 chore: upstream tail-recursive implementations of List operations, and @[csimp] lemmas (#3785)
• 2405fd6 feat: trace non-easy whnf invocations (#3774)
• 63290ba chore: update stage0