Checker "lazylean" on test "other/inductive-undeclared-universe"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: other/inductive-undeclared-universe · Expected: ✋ reject · Size: 2.5 KB · Lines: 42 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 54.4 ms · instructions: 6.5 M · max rss memory: 21.1 MB · run 2026-10-30 14:18:02 UTC
stderr:
loaded 4 declarations, 24 exprs (24 unique), 12 names in 0.000219619s declaration order verified in 3.029e-06s environment built in 1.912e-05s; checking with 4 worker processes FAIL U (line 38): invalid reference to undefined universe level parameter 'u' checked 0 declarations, 1 failed, in 0.00491465s wall (3.01796e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker