lean4-htt

Author SHA1 Message Date

Author	SHA1	Message	Date
Marc Huisinga	168c125cf5	chore: relative lean-toolchains (#12652 ) This PR changes all `lean-toolchain` to use relative toolchain paths instead of `lean4` and `lean4-stage0` identifiers, which removes the need for manually linking toolchains via Elan. After this PR, at least Elan 4.2.0 and 0.0.224 of the Lean VS Code extension will be needed to edit core. Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>	2026-02-25 10:23:35 +00:00
Wojciech Różowski	7d32030729	feat: add `cbv_eval` attribute (#12296 ) This PR adds `cbv_eval` attribute that allows to evaluate functions in `cbv` tactic using pre-registered theorems.	2026-02-10 15:41:42 +00:00

Marc Huisinga

168c125cf5

chore: relative lean-toolchains (#12652 )

This PR changes all `lean-toolchain` to use relative toolchain paths
instead of `lean4` and `lean4-stage0` identifiers, which removes the
need for manually linking toolchains via Elan.

After this PR, at least Elan 4.2.0 and 0.0.224 of the Lean VS Code
extension will be needed to edit core.

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>

2026-02-25 10:23:35 +00:00

Wojciech Różowski

7d32030729

feat: add cbv_eval attribute (#12296 )

This PR adds `cbv_eval` attribute that allows to evaluate functions in
`cbv` tactic using pre-registered theorems.

2026-02-10 15:41:42 +00:00

2 commits