commit: c970c74d66b8dda94b3d6efb7f722ee111ca3f7b

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

Sat Aug 09 19:19:29 2025 +0200
committer: GitHub <noreply@github.com>

Sat Aug 09 17:19:29 2025 +0000
tree: c89cfb517a5b485abe7619e31265d79177b8f54e
parent: 479da83f577c19b18ba05288b57ac40c9384b9ab [diff]

feat: introduce `Lean.realizeValue` for sharing computation results between compatible environment branches (#9798)

This PR introduces `Lean.realizeValue`, a new metaprogramming API for
parallelism-aware caching of `MetaM` computations

4 files changed

tree: c89cfb517a5b485abe7619e31265d79177b8f54e

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.