commit: b49f156f3378c5b705f5ba8742d97f0a51aa766f

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

Tue Jun 04 09:34:48 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Jun 04 09:35:35 2024 -0700
tree: c61cc38edccb56ac65294a82f81fffb14f690cb2
parent: 8437d1f660915e9e8f6789be4399b8d3ab6d9a79 [diff]

fix: panic when applying `@[simp]` to malformed theorem syntax

closes #4309

src/Lean/Elab/Term.lean[diff]
tests/lean/4309.lean[Added - diff]
tests/lean/4309.lean.expected.out[Added - diff]

3 files changed

tree: c61cc38edccb56ac65294a82f81fffb14f690cb2

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).