Checker "lazylean" on test "corner-cases/imax-nested-absorption"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: corner-cases/imax-nested-absorption · Expected: 🤷 either · Size: 736 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Result: ✋ rejected · exit code 1 · wall time: 45.5 ms · instructions: 6.3 M · max rss memory: 21.4 MB · run 2026-11-01 13:14:47 UTC
stderr:
loaded 2 declarations, 3 exprs (3 unique), 4 names in 6.6834e-05s declaration order verified in 1.574e-06s environment built in 1.0887e-05s; checking with 4 worker processes FAIL imaxAbsorbRight (line 12): declaration type mismatch for 'imaxAbsorbRight' inferred: Sort((imax u v)+1) declared: Sort((imax (imax u v) v)+1) checked 0 declarations, 1 failed, in 0.00129064s wall (8.3601e-07 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker