Lean Kernel Arena / tenet-jvm / corner-cases/eta-rule-k

Checker: tenet-jvm · Version: 0.1.3 · 📄 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: 91.6 ms · instructions: 682.9 M · max rss memory: 64.8 MB · run 2026-10-24 17:12:50 UTC

stdout:

REJECTED DEF etaRuleK: declaration type mismatch, etaRuleK
  value 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))
  but is expected to have 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) (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))
lean 4.34.1, export format 3.1.0, 121 lines
checked 7 constants ({}) and 2 inductive blocks in 0.04s
axioms declared: none
1 declaration(s) rejected