`debug_assert!` expression is not checked when `debugAssertions` is disabled

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Currently with debugAssertions option disabled debug_assert! accepts everything that parses.

Steps to Reproduce

1. debug_assert! '1' + 2
2. debugAssertions option is disabled

Expected behavior: macro throws an error signaling that the expression is invalid.

Actual behavior: macro discards the expression silently.

Versions

Lean 4.32.0

Additional Information

Equivalent macro in Rust always performs type checking.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal reproduction debug_assert! '1' + 2 in a Lean nightly environment, with debugAssertions disabled, and inspect the debug_assert! macro entry point and related tests. Confirm the behavior with the option both enabled and disabled. Done means the invalid expression is rejected even when assertions are disabled, while valid expressions retain the expected behavior.