commit: 91598bd7f852e175ff1fc65e565f75271b52d865

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Wed Mar 25 19:13:23 2026 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Mar 25 19:13:23 2026 -0700
tree: 98d6a8fa9815162770b0cf905ee12390526e0801
parent: 72a0605ac5d69b18d36b228ece96a455d1c70712 [diff]

refactor: move `reportDbgIssue!` from grind to SymM

This PR moves `reportDbgIssue!` and `expandReportDbgIssueMacro` from
`Grind/Types.lean` to `SymM.lean`. The macro now checks `sym.debug`
instead of `grind.debug`, since debug issue reporting is a Sym-level
concern shared across all modules in a `sym =>` block.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

4 files changed

tree: 98d6a8fa9815162770b0cf905ee12390526e0801

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.