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

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

Closed leodemoura closed 1 week ago

leodemoura commented 1 week ago

This PR also fixes:

leanprover-community-mathlib4-bot commented 1 week ago

Mathlib CI status (docs):

❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 26a1b934c226c6aa923248804ba92c23f56c5115 --onto e362b50fa95d6823e59dd706803a93c25e888535. (2024-05-06 18:54:59)

digama0 commented 1 week ago

Does this fix #3499 as well?

leodemoura commented 1 week ago

Does this fix #3499 as well?

No.