commit: ed534b96dbbc714c79e9572c7f16a005f8eb5ca3

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

Wed May 22 14:16:20 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Wed May 22 14:48:49 2024 -0700
tree: 35706831536ae4ee31dd926267605bdfe2193a85
parent: ff37e5d512efcd3981290270a2fc3ecb100bbd0c [diff]

fix: `case` tactic in macros

We must erase macro scopes for tags in `case` as we do in `cases
.. with ..` and `induction .. with ..`.

2 files changed

tree: 35706831536ae4ee31dd926267605bdfe2193a85

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