Lean Kernel Arena / ind-models / corner-cases/eta-ctor

Checker "ind-models" on test "corner-cases/eta-ctor"

Checker: ind-models · Version: 86caadd · 📄 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: 76.5 ms · instructions: 604.7 M · max rss memory: 108.4 MB · run 2026-10-24 16:43:17 UTC

stderr:
/home/runner/work/lean-kernel-arena/lean-kernel-arena/_build/tests/corner-cases/eta-ctor.ndjson: input kernel check rejected: [etaCtor]: (kernel) declaration type mismatch, 'etaCtor' has type
  ∀ (x : True → T), Eq x x
but it is expected to have type
  ∀ (x : True → T), Eq (T.mk (x True.intro).val) x