Lean Kernel Arena / eink0rn / corner-cases/eta-ctor

Checker: eink0rn · Version: 1.1.6 · 📄 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: 12.5 ms · instructions: 9.7 M · max rss memory: 12.0 MB · run 2026-10-24 16:43:29 UTC

stdout:

REJECT

stderr:

etaCtor: type mismatch:
  term     fun (x : (proof : True) -> T) => Eq.refl.{1} ((proof : True) -> T) #0
  has type (x : (proof : True) -> T) -> Eq.{1} ((proof : True) -> T) #0 #0
  expected (x : (proof : True) -> T) -> Eq.{1} ((proof : True) -> T) (T.mk (T.val (#0 True.intro))) #0