Checker "lazylean" on test "bugs/unit-rec-rule"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: bugs/unit-rec-rule · Expected: ✋ reject · Size: 3.0 KB · Lines: 54 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 15.5 ms · instructions: 6.7 M · max rss memory: 21.2 MB · run 2026-10-27 12:09:39 UTC
stderr:
loaded 4 declarations, 30 exprs (30 unique), 15 names in 0.000108209s declaration order verified in 3.91e-06s environment built in 1.3125e-05s; checking with 4 worker processes FAIL FAIL PUnitEmptyProp (line (line 2642): ): recursor 'PUnit.rec': rule for 'PUnit.unit' differs from the derived rulerecursor 'EmptyProp.rec' elimination universe is named 'u_2', expected 'u' checked 0 declarations, 2 failed, in 0.00206212s wall (9.8193e-07 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker