logos-kernel on bugs/constlevels

Checker "logos-kernel" on test "bugs/constlevels"

Checker: logos-kernel · Version: 1e6ad5b · 📄 Declaration · 🔗 Source

Test: bugs/constlevels · Expected: ✋ reject · Size: 15.3 KB · Lines: 283 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Result: ✋ rejected · exit code 1 · wall time: 2.81 ms · instructions: 3.0 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:

rejected: declaration '_test': let value type mismatch
  in `let x0 : Nat := Nat; let x1 : Eq := let x1 : Eq := (let x1 : x0 Nat := Eq; x1) Eq (x0 Nat); let x2 : false_ne_true (let x2 : x1 Nat := Eq; x2) := Eq.casesOn; x2 Nat; let x2 : Eq := (let x2 : x1 Nat := Eq; x2) Eq (x1 Nat); let x3 : false_ne_true (let x3 : x2 Nat := Eq; x3) := Eq.casesOn; x3 Nat`
  expected type: Nat
  but the value has type: Sort LevelId(1)