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

Checker: lazylean · Version: 0.3.0 · 📄 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: 15.1 ms · instructions: 7.1 M · max rss memory: 21.2 MB · run 2026-10-24 16:35:57 UTC

stderr:

loaded 3 declarations, 85 exprs (85 unique), 29 names in 0.000117284s
declaration order verified in 1.884e-06s
environment built in 2.2293e-05s; checking with 4 worker processes
FAIL etaRuleK (line 121): declaration type mismatch for 'etaRuleK'
  inferred: ((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))
  declared: ((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))
checked 2 declarations, 1 failed, in 0.00200494s wall (1.27808e-06 core-hours over 4 workers); 0 reduction steps; peak 19 MB in one worker