Checker "eink0rn" on test "corner-cases/alg-conv-trans-acc"
Checker: eink0rn · Version: 1.1.6 · 📄 Declaration · 🔗 Source
Test: corner-cases/alg-conv-trans-acc · Expected: 🤷 either · Size: 66.4 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Result: ✋ rejected · exit code 1 · wall time: 16.1 ms · instructions: 26.6 M · max rss memory: 17.5 MB · run 2026-10-24 16:43:29 UTC
stdout:
REJECT
stderr:
trans: type mismatch:
term fun (a : Acc.{1} Nat (fun (x1._@.Test.1043551373._hygCtx._hyg.6 : Nat) => fun (x2._@.Test.1043551373._hygCtx._hyg.6 : Nat) => LT.lt.{0} Nat instLTNat #1 #0) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => Eq.refl.{1} Bool (f (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) #0)
has type (a : Acc.{1} Nat (fun (x1._@.Test.1043551373._hygCtx._hyg.6 : Nat) => fun (x2._@.Test.1043551373._hygCtx._hyg.6 : Nat) => LT.lt.{0} Nat instLTNat #1 #0) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) -> Eq.{1} Bool (f (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) #0) (f (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) #0)
expected (a : Acc.{1} Nat (fun (x1._@.Test.1043551373._hygCtx._hyg.6 : Nat) => fun (x2._@.Test.1043551373._hygCtx._hyg.6 : Nat) => LT.lt.{0} Nat instLTNat #1 #0) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) -> Eq.{1} Bool (f (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) #0) (f (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (Acc.inv.{1} Nat (fun (x1._@.Test.1043551373._hygCtx._hyg.6 : Nat) => fun (x2._@.Test.1043551373._ ...