commit: a2fc336cfe15dbd602c4407fcc8182eb4c5f092d

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

Fri May 10 17:18:15 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Fri May 10 17:19:57 2024 -0700
tree: 9b4f206d2f77eb978809b254cfb99819dca8c807
parent: fe7b96d8a0cf85e1ea81791ac9d673f84c9e866d [diff]

fix: auto/option params should not break `sorry`

closes #2649

src/Lean/Elab/BuiltinNotation.lean[diff]
tests/lean/run/2649.lean[Added - diff]

2 files changed

tree: 9b4f206d2f77eb978809b254cfb99819dca8c807

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).