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

Checker: rpylean · Version: v2026.9.1 · 📄 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: 3.83 ms · instructions: 3.0 M · max rss memory: 4.0 MB · run 2026-10-27 12:16:10 UTC

stderr:

recursor PUnit.rec.{u_1, u} : {motive : PUnit → Sort u_1} → motive PUnit.unit → (t : PUnit) → motive t
rule for PUnit.unit rhs head is not the corresponding minor (expected bvar #0)
theorem badR : PUnit.rec EmptyProp PUnit.unit :=
                                   ^^^^^^^^^^
                                   has type
                                     PUnit
                                   but is expected to have type
                                     PUnit.rec EmptyProp PUnit.unit
theorem boom : EmptyProp :=
  badR
  ^^^^
  has type
    PUnit.rec EmptyProp PUnit.unit
  but is expected to have type
    EmptyProp
summary: 7/7 decls checked, peak 32 MB, allocated 0 MB, heartbeats 0
checked in 0.000263s