commit: b995b09307c8bf2543aa5821e01eff173df7aa98

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

Thu Jul 30 18:35:58 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Jul 30 18:43:40 2026 +0000
tree: 902b19318b175c8b72d5c8e5a89442c0a8fdc65d
parent: fd1cec3b99e4887d59c833a52691e3ba4cd5d40d [diff]

fix: check universe parameters in mutual definitions

This PR checks that declarations in a mutual block use the same
universe parameters. The elaborator already enforces this invariant,
but meta-programming can bypass it.

src/kernel/environment.cpp[diff]
tests/elab/mutualLevelParams.lean[Added - diff]

2 files changed

tree: 902b19318b175c8b72d5c8e5a89442c0a8fdc65d

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.