Lean Kernel Arena / tenet / corner-cases/subject-reduction-reduct

Checker: tenet · Version: 0.11.3 · 📄 Declaration · 🔗 Source

Test: corner-cases/subject-reduction-reduct · Expected: 🤷 either · Size: 65.5 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Result: ✋ rejected · exit code 1 · wall time: 151 ms · instructions: 913.5 M · max rss memory: 47.1 MB · run 2026-10-24 16:42:18 UTC

stdout:

FAIL def reduct (0.00s)
    application type mismatch in
      k x0
    argument has type
      D (f (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) a)
    but function has type
      D (f (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (redex._proof_1 a)) → Unit
FAILED: 40 checked, 1 failed, 0 skipped, 66 constants, 0.1s, 4 jobs