Checker "lazylean" on test "bugs/pi-closure-context"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: bugs/pi-closure-context · Expected: ✋ reject · Size: 1.5 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.35.0 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 15.0 ms · instructions: 6.4 M · max rss memory: 21.2 MB · run 2026-10-27 15:31:19 UTC
stderr:
loaded 5 declarations, 15 exprs (15 unique), 5 names in 7.4476e-05s declaration order verified in 2.036e-06s environment built in 1.2192e-05s; checking with 4 worker processes FAIL bad (line 23): declaration type mismatch for 'bad' inferred: (([anonymous] : TrueTy) -> Sort(0)) declared: (([anonymous] : TrueTy) -> FalseTy) checked 3 declarations, 1 failed, in 0.00129012s wall (8.60921e-07 core-hours over 4 workers); 1 reduction steps; peak 19 MB in one worker