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

Checker: lean4lean · Version: arena (bce3448) · 📄 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: 27.9 ms · instructions: 192.6 M · max rss memory: 99.2 MB · run 2026-10-24 16:25:16 UTC

stderr:

uncaught exception: at bad: (kernel) application type mismatch
  _private.Test.0.propRepresentationFalse _private.Test.0.badProp fun b => b
argument has type
  Bool → Bool
but function has type
  (encode : Bool → _private.Test.0.badProp) →
    (decode : _private.Test.0.badProp → Bool) →
      @Eq Bool (decode (encode Bool.false)) Bool.false → @Eq Bool (decode (encode Bool.true)) Bool.true → False