Lean Kernel Arena / eink0rn / bugs/unit-rec-rule

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

Test: bugs/unit-rec-rule · Expected: ✋ reject · Size: 3.0 KB · Lines: 54 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration

Result: ✋ rejected · exit code 1 · wall time: 7.63 ms · instructions: 8.0 M · max rss memory: 11.4 MB · run 2026-10-27 12:10:55 UTC

stdout:

REJECT

stderr:

PUnit: the declared reduction rule for PUnit.unit is not the one iota gives
  declared fun (motive : (t : PUnit.{u}) -> Sort u_1) => fun (unit : #0 PUnit.unit.{u}) => PUnit.unit.{u}
  derived  fun (motive : ([anonymous] : PUnit.{u}) -> Sort u_1) => fun (minor.1 : #0 PUnit.unit.{u}) => #0