Checker "lazylean" on test "corner-cases/large-elim-maybe-prop"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: corner-cases/large-elim-maybe-prop · Expected: 🤷 either · Size: 3.1 KB · Lines: 55 · lean4export: 3.1.0 · Lean: 4.35.0 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 12.8 ms · instructions: 6.6 M · max rss memory: 21.3 MB · run 2026-11-01 13:14:47 UTC
stderr:
loaded 2 declarations, 39 exprs (39 unique), 11 names in 8.531e-05s declaration order verified in 6.085e-06s environment built in 1.1849e-05s; checking with 4 worker processes FAIL MaybePropBox (line 42): recursor 'MaybePropBox.rec' should only eliminate into Prop checked 1 declarations, 1 failed, in 0.00176399s wall (1.18463e-06 core-hours over 4 workers); 1 reduction steps; peak 19 MB in one worker