Lean Kernel Arena / eink0rn / corner-cases/eta-rec-struct

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

Test: corner-cases/eta-rec-struct · Expected: 🤷 either · Size: 9.5 KB · Lines: 174 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

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

stdout:

REJECT

stderr:

etaRecStruct: type mismatch:
  term     fun (a : (a._@._internal._hyg.0 : Prod.{0, 0} Bool Bool) -> Bool) => Eq.refl.{1} ((a._@._internal._hyg.0 : Prod.{0, 0} Bool Bool) -> Bool) #0
  has type (a : (a._@._internal._hyg.0 : Prod.{0, 0} Bool Bool) -> Bool) -> Eq.{1} ((a._@._internal._hyg.0 : Prod.{0, 0} Bool Bool) -> Bool) #0 #0
  expected (a : (a._@._internal._hyg.0 : Prod.{0, 0} Bool Bool) -> Bool) -> Eq.{1} ((a._@._internal._hyg.0 : Prod.{0, 0} Bool Bool) -> Bool) (Prod.rec.{1, 0, 0} Bool Bool (fun (x._@.Test.3091511195._hygCtx._hyg.21 : Prod.{0, 0} Bool Bool) => Bool) (fun (b : Bool) => fun (c : Bool) => #2 (Prod.mk.{0, 0} Bool Bool #1 #0))) #0