Checker "lazylean" on test "bugs/closure-level-subst"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: bugs/closure-level-subst · Expected: ✋ reject · Size: 4.0 KB · Lines: 74 · lean4export: 3.1.0 · Lean: 4.35.0 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 45.5 ms · instructions: 6.6 M · max rss memory: 21.2 MB · run 2026-10-27 15:31:19 UTC
stderr:
loaded 14 declarations, 40 exprs (40 unique), 15 names in 8.9796e-05s
declaration order verified in 4.071e-06s
environment built in 1.3155e-05s; checking with 4 worker processes
FAIL lower (line 53): declaration type mismatch for 'lower'
inferred: Family.{1}
declared: Family.{0}
checked 8 declarations, 1 failed, in 0.00148871s wall (9.21481e-07 core-hours over 4 workers); 6 reduction steps; peak 19 MB in one worker