chore: add test for imax 1 u normalization

arthur-adjedj · arthur-adjedj · commit 5c816c68e0b6 · 2025-03-10T14:39:59.000Z
diff --git a/tests/lean/run/7096.lean b/tests/lean/run/7096.lean
@@ -0,0 +1,9 @@
+/-!
+# Normalization of imax 1 u
+
+https://github.com/leanprover/lean4/issues/7096
+
+Universe levels of the form `imax 1 u` should normalize to `u`.
+-/
+
+example (α : Sort u) : Sort u := Unit → α
