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

Checker: tenet · Version: 0.11.3 · 📄 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: 132 ms · instructions: 791.8 M · max rss memory: 44.6 MB · run 2026-10-27 12:11:50 UTC

stdout:

FAIL inductive PUnit (0.02s)
    'PUnit.rec': exported rule 0 rhs does not match the kernel's
      exported: fun (motive : PUnit.{u} → Sort u_1) => fun (unit : motive PUnit.unit.{u}) => PUnit.unit.{u}
      kernel:   fun (motive : PUnit.{u} → Sort u_1) => fun (unit : motive PUnit.unit.{u}) => unit
FAIL inductive EmptyProp (0.02s)
    'EmptyProp.rec': exported universe parameters does not match the kernel's
      exported: [u_2]
      kernel:   [u]
FAIL thm badR (0.02s)
    declaration type mismatch for 'badR'
      expected: PUnit.rec.{1, 0} (fun ([anonymous] : PUnit.{0}) => Prop) EmptyProp PUnit.unit.{0}
      inferred: PUnit.{0}
FAIL thm boom (0.02s)
    declaration type mismatch for 'boom'
      expected: EmptyProp
      inferred: PUnit.rec.{1, 0} (fun ([anonymous] : PUnit.{0}) => Prop) EmptyProp PUnit.unit.{0}
FAILED: 0 checked, 4 failed, 0 skipped, 7 constants, 0.1s, 4 jobs