feat: add letConfig support to do block let/have

[sgraf812]

This PR adds support for let configuration options ((eq := h), +nondep, +usedOnly, +zeta) in do block let and have declarations, matching the behavior available in term-level let/have. Configuration options are rejected with let mut since they are incompatible with mutable bindings. +postponeValue and +generalize are also rejected in do blocks.

Parser changes add letConfig to doLet, doLetElse, doLetArrow, and doHave. Both the legacy and new do elaborators are updated with backward-compatible index handling (stage0 macros may produce old-shape syntax without letConfig).

Example usage:

do
  let (eq := h) x := "hello"
  -- h : x = "hello" is available
  have : x = "hello" := h
  return x

🤖 Generated with Claude Code

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-31 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-31 14:46:46)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-31 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-31 14:46:48)

[sgraf812]

#13255