Lean Kernel Arena / tenet-jvm / corner-cases/eta-ctor

Checker: tenet-jvm · Version: 0.1.3 · 📄 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: 89.2 ms · instructions: 677.9 M · max rss memory: 64.8 MB · run 2026-10-24 17:12:50 UTC

stdout:

REJECTED DEF etaCtor: declaration type mismatch, etaCtor
  value has type: (? a : (? proof : True, T), (Eq.{[1]} (? proof : True, T) #0 #0))
  but is expected to have type: (? x : (? proof : True, T), (Eq.{[1]} (? proof : True, T) (T.mk (T.val (#0 True.intro))) #0))
lean 4.34.1, export format 3.1.0, 148 lines
checked 14 constants ({DEF=1}) and 4 inductive blocks in 0.04s
axioms declared: none
1 declaration(s) rejected