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

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

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

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

stdout:

REJECT

stderr:

unitLikePi: type mismatch:
  term     fun (α : Sort 1) => fun (p : (a._@._internal._hyg.0 : #0) -> Unit) => fun (q : (a._@._internal._hyg.0 : #1) -> Unit) => Eq.refl.{1} ((a._@._internal._hyg.0 : #2) -> Unit) #0
  has type (α : Sort 1) -> (p : (a._@._internal._hyg.0 : #0) -> Unit) -> (q : (a._@._internal._hyg.0 : #1) -> Unit) -> Eq.{1} ((a._@._internal._hyg.0 : #2) -> Unit) #0 #0
  expected (α : Sort 1) -> (p : (a._@._internal._hyg.0 : #0) -> Unit) -> (q : (a._@._internal._hyg.0 : #1) -> Unit) -> Eq.{1} ((a._@._internal._hyg.0 : #2) -> Unit) #1 #0