commit: c3863f743166b12fbfff4cb98706baec3384a896

[log]
author: Kyle Miller <kmill31415@gmail.com>

Mon May 18 23:51:31 2026 -0700
committer: Kyle Miller <kmill31415@gmail.com>

Mon May 18 23:51:31 2026 -0700
tree: 1d5028fcffc0b364fa4abbd1b601c7a9f41dde09
parent: 43ef70db63e2c1c1720b84fd153125c96a00c5d2 [diff]

refactor: avoid `liftCommandElabM` in `@[ext]`

This PR eliminates the use of `liftCommandElabM` in the `@[ext]` attribute, since it is unnecessary — all the computations can stay in `TermElabM`.

src/Lean/Elab/Tactic/Ext.lean[diff]

1 file changed

tree: 1d5028fcffc0b364fa4abbd1b601c7a9f41dde09

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.