Lean Kernel Arena / eink0rn / corner-cases/eta-unit-like-nested

Checker: eink0rn · Version: 1.1.6 · 📄 Declaration · 🔗 Source

Test: corner-cases/eta-unit-like-nested · Expected: 🤷 either · Size: 16.0 KB · Lines: 256 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Result: ✋ rejected · exit code 1 · wall time: 12.7 ms · instructions: 11.7 M · max rss memory: 12.8 MB · run 2026-10-24 16:43:29 UTC

stdout:

REJECT

stderr:

unitLikeNested: type mismatch:
  term     fun (p : Mixed Nat ((a._@._internal._hyg.0 : Bool) -> UnitField)) => fun (q : Mixed Nat ((a._@._internal._hyg.0 : Bool) -> UnitField)) => Eq.refl.{1} (Mixed Nat ((a._@._internal._hyg.0 : Bool) -> UnitField)) #0
  has type (p : Mixed Nat ((a._@._internal._hyg.0 : Bool) -> UnitField)) -> (q : Mixed Nat ((a._@._internal._hyg.0 : Bool) -> UnitField)) -> Eq.{1} (Mixed Nat ((a._@._internal._hyg.0 : Bool) -> UnitField)) #0 #0
  expected (p : Mixed Nat ((a._@._internal._hyg.0 : Bool) -> UnitField)) -> (q : Mixed Nat ((a._@._internal._hyg.0 : Bool) -> UnitField)) -> Eq.{1} (Mixed Nat ((a._@._internal._hyg.0 : Bool) -> UnitField)) #1 #0