commit: 0e28043ec6749ab227d84b690fbb10375dcf714c

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

Sun Jan 25 15:16:30 2026 -0800
committer: GitHub <noreply@github.com>

Sun Jan 25 23:16:30 2026 +0000
tree: 832d7004c6e5e8999ab111fe9b2770c324f31be3
parent: 45862d548620bcb8c865e7de084b79ac3f62cd5c [diff]

feat: add `simpTelescope` simproc for simplifying binders before intro (#12154)

This PR adds `simpTelescope`, a simproc that simplifies telescope
binders (`have`-expression values and arrow hypotheses) but not the
final body. This is useful for simplifying targets before introducing
hypotheses.

6 files changed

tree: 832d7004c6e5e8999ab111fe9b2770c324f31be3

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.