Checker "lazylean" on test "bugs/nested-rec-rule-nfields"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: bugs/nested-rec-rule-nfields · Expected: ✋ reject · Size: 39.9 KB · Lines: 728 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Result: ✋ rejected · exit code 1 · wall time: 14.8 ms · instructions: 11.1 M · max rss memory: 21.3 MB · run 2026-10-24 16:35:57 UTC
stderr:
loaded 23 declarations, 551 exprs (551 unique), 145 names in 0.000194744s declaration order verified in 6.262e-06s environment built in 2.7644e-05s; checking with 4 worker processes FAIL T (line 651): recursor 'T.rec': rule 1 constructor/field data differs checked 22 declarations, 1 failed, in 0.00325427s wall (2.78351e-06 core-hours over 4 workers); 66 reduction steps; peak 20 MB in one worker