Lean Kernel Arena / rpylean / bugs/nested-rec-rule-nfields

Checker: rpylean · Version: v2026.9.1 · 📄 Declaration · 🔗 Source

Test: bugs/nested-rec-rule-nfields · Expected: ✋ reject · Size: 39.9 KB · Lines: 728 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Result: ✋ rejected · exit code 1 · wall time: 4.71 ms · instructions: 8.9 M · max rss memory: 5.8 MB · run 2026-10-24 17:12:35 UTC

stderr:

recursor T.rec.{u} : {motive_1 : T → Sort u} →
  {motive_2 : C T → Sort u} →
    motive_1 T.base →
      ((a : C T) → (a : ∀ (a : Type), Prop) → motive_2 a → motive_1 (T.mk a a)) →
        ((a : T) → motive_1 a → motive_2 (C.c a)) → (t : T) → motive_1 t
rule for T.mk claims 1 fields but the ctor has 2
summary: 41/41 decls checked, peak 32 MB, allocated 0 MB, heartbeats 0
checked in 0.000966s