Checker "tenet" on test "bugs/level-imax-leq"
Checker: tenet · Version: 0.11.3 · 📄 Declaration · 🔗 Source
Test: bugs/level-imax-leq · Expected: ✋ reject · Size: 5.6 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 117 ms · instructions: 804.2 M · max rss memory: 44.6 MB · run 2026-10-24 16:42:18 UTC
stdout:
FAIL inductive False (0.02s)
'False.rec': exported universe parameters does not match the kernel's
exported: [u_1]
kernel: [u]
FAIL inductive True (0.02s)
'True.rec': exported universe parameters does not match the kernel's
exported: [u_1]
kernel: [u]
FAIL inductive Bool (0.02s)
'Bool.rec': exported universe parameters does not match the kernel's
exported: [u_1]
kernel: [u]
FAIL def down (0.02s)
declaration type mismatch for 'down'
expected: Sort ((imax u v)+1) → Sort (imax u v)
inferred: Sort ((imax u v)+1) → Sort ((imax u v)+1)
FAILED: 1 checked, 4 failed, 0 skipped, 11 constants, 0.1s, 4 jobs