commit: 2579c8542feaba0e23a3c57aac6bcb66752368af

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

Sun Mar 22 10:28:43 2026 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Sun Mar 22 10:32:37 2026 -0700
tree: 139c88c85b0559c34dd6e11b1cac760447533704
parent: c9708e7bd7cf47106e2fc063d3c586c8f333e54d [diff]

feat: add sanity checks to `register_sym_simp`

This PR adds validation to the `register_sym_simp` command:
- reject duplicate variant names
- validate `pre`/`post` syntax by elaborating them via `elabSymSimproc`
  in a minimal `GrindTacticM` context, catching unknown theorem names
  and unknown theorem set references at registration time

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

2 files changed

tree: 139c88c85b0559c34dd6e11b1cac760447533704

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.