commit: c35526970f12013abdd6f26175f0d672374ed1e8

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

Mon May 06 11:32:08 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Mon May 06 11:37:16 2024 -0700
tree: 7101c311cb66dfa4edd7d1e5c65790bc37eb44fc
parent: 26a1b934c226c6aa923248804ba92c23f56c5115 [diff]

fix: code duplication at `liftCoreM` and `liftTermElabM` at `Command.lean`

This PR also
- Fields caching specific `Options` at `CoreM` are properly set.
- `nextMacroScope` was not being propagated at `liftCoreM`.

2 files changed

tree: 7101c311cb66dfa4edd7d1e5c65790bc37eb44fc

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 (documentation source: doc/make/index.md).