max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta/Constructions
History
Joachim Breitner 5ad5c2cf04
fix: universe level in .below and .brecOn construction (#4651) 
I made a mistake in #4517, fixed here, so about time to add a test.

I wonder if this generic level optimization should be moved into
`mkLevelMax'`, but not today.

fixes #4650
2024-07-04 18:19:43 +00:00
..
BRecOn.lean fix: universe level in .below and .brecOn construction (#4651) 2024-07-04 18:19:43 +00:00
RecOn.lean