Lean Kernel Arena / eink0rn / corner-cases/eta-rule-k

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

Test: corner-cases/eta-rule-k · Expected: 🤷 either · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

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

stdout:

REJECT

stderr:

etaRuleK: type mismatch:
  term     fun (a : (a._@._internal._hyg.0 : Eq.{1} Bool Bool.true Bool.true) -> Bool) => Eq.refl.{1} ((a._@._internal._hyg.0 : Eq.{1} Bool Bool.true Bool.true) -> Bool) #0
  has type (a : (a._@._internal._hyg.0 : Eq.{1} Bool Bool.true Bool.true) -> Bool) -> Eq.{1} ((a._@._internal._hyg.0 : Eq.{1} Bool Bool.true Bool.true) -> Bool) #0 #0
  expected (a : (a._@._internal._hyg.0 : Eq.{1} Bool Bool.true Bool.true) -> Bool) -> Eq.{1} ((a._@._internal._hyg.0 : Eq.{1} Bool Bool.true Bool.true) -> Bool) (Eq.rec.{1, 1} Bool Bool.true (fun (x._@.Test.1420384072._hygCtx._hyg.30 : Bool) => fun (x._@.Test.1420384072._hygCtx._hyg.32 : Eq.{1} Bool Bool.true #0) => Bool) (#0 (Eq.refl.{1} Bool Bool.true)) Bool.true) #0