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

Checker: official · Version: v4.34.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: 26.7 ms · instructions: 190.3 M · max rss memory: 67.1 MB · run 2026-10-24 17:05:28 UTC

stderr:

uncaught exception: while replaying declaration '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