commit: dd745fac5701038810402335da788b4db39b2a78

[log]
author: Sebastian Ullrich <sebasti@nullri.ch>

Tue Oct 20 16:19:17 2026 +0000
committer: Sebastian Ullrich <sebasti@nullri.ch>

Tue Oct 20 16:22:29 2026 +0000
tree: c156d03172979d7f46ac119a3ecf671f4a2e2b2a
parent: fed6d15e6b3f5f1e0797cc95268415e2f4dc3aad [diff]

feat: make `cbv` simplifier methods public

This PR makes `mkCbvMethods`, `cbvPre`, and `cbvPost` public so that users can run `cbv` from their own `SimpM` session, e.g. to evaluate several terms with a shared cache or to combine `cbv` with their own simprocs.

`Lean.Meta.Tactic.Cbv.CbvSimproc` becomes a public import of `Lean.Meta.Tactic.Cbv.Main` since `CbvSimprocs` now appears in public signatures.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

2 files changed

tree: c156d03172979d7f46ac119a3ecf671f4a2e2b2a

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.