Checker "lazylean" on test "corner-cases/eta-ctor"
Checker: lazylean · Version: 0.3.0 · 📄 Declaration · 🔗 Source
Test: corner-cases/eta-ctor · Expected: 🤷 either · Size: 9.0 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Result: ✋ rejected · exit code 1 · wall time: 15.1 ms · instructions: 7.3 M · max rss memory: 21.2 MB · run 2026-10-24 16:35:57 UTC
stderr:
loaded 6 declarations, 104 exprs (104 unique), 34 names in 0.000163262s
declaration order verified in 2.244e-06s
environment built in 1.7604e-05s; checking with 4 worker processes
FAIL etaCtor (line 148): declaration type mismatch for 'etaCtor'
inferred: ((a : ((proof : True) -> T)) -> (((Eq.{1} ((proof : True) -> T)) #0) #0))
declared: ((x : ((proof : True) -> T)) -> (((Eq.{1} ((proof : True) -> T)) (T.mk (T.val (#0 True.intro)))) #0))
checked 5 declarations, 1 failed, in 0.002049s wall (1.56229e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker