Checker "lazylean" on test "bugs/loose-bvar-value"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: bugs/loose-bvar-value · Expected: ✋ reject · Size: 2.7 KB · Lines: 48 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 61.6 ms · instructions: 6.4 M · max rss memory: 21.3 MB · run 2026-10-27 12:09:39 UTC
stderr:
loaded 2 declarations, 31 exprs (31 unique), 11 names in 0.000204646s declaration order verified in 2.978e-06s environment built in 1.8218e-05s; checking with 4 worker processes FAIL f (line 9): declaration 'f' has loose bound variables checked 0 declarations, 1 failed, in 0.00287255s wall (1.56634e-06 core-hours over 4 workers); 0 reduction steps; peak 18 MB in one worker