Checker "lazylean" on test "corner-cases/imax-right-successor"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: corner-cases/imax-right-successor · Expected: 🤷 either · Size: 806 B · Lines: 21 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Result: ✋ rejected · exit code 1 · wall time: 14.0 ms · instructions: 6.3 M · max rss memory: 21.1 MB · run 2026-10-24 16:35:57 UTC
stderr:
loaded 2 declarations, 4 exprs (4 unique), 4 names in 0.000106852s declaration order verified in 1.823e-06s environment built in 1.082e-05s; checking with 4 worker processes FAIL imaxRightOne (line 11): declaration type mismatch for 'imaxRightOne' inferred: Sort((imax u 1)+1) declared: Sort((max u 1)+1) checked 0 declarations, 1 failed, in 0.00157067s wall (1.03601e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker