Lean Kernel Arena / ind-models / bugs/unit-rec-rule

Checker "ind-models" on test "bugs/unit-rec-rule"

Checker: ind-models · Version: 86caadd · 📄 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: 89.6 ms · instructions: 600.0 M · max rss memory: 109.1 MB · run 2026-10-27 12:13:16 UTC

stderr:
/home/runner/work/lean-kernel-arena/lean-kernel-arena/_build/tests/bugs/unit-rec-rule.ndjson: input kernel check rejected: [badR]: (kernel) declaration type mismatch, 'badR' has type
  PUnit
but it is expected to have type
  PUnit.rec EmptyProp PUnit.unit