Checker "eink0rn" on test "bugs/proj-of-stuck-prop"
Checker: eink0rn · Version: 1.1.6 · 📄 Declaration · 🔗 Source
Test: bugs/proj-of-stuck-prop · Expected: ✋ reject · Size: 275.7 KB · Lines: 5.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Result: ✋ rejected · exit code 1 · wall time: 17.1 ms · instructions: 74.3 M · max rss memory: 29.6 MB · run 2026-10-24 16:43:29 UTC
stdout:
REJECT
stderr:
Native64ResultSortOwner: inductive Native64ResultSortOwner: the type must end in a sort, got Native64ResultSortGate.rec.{2} x!14 (fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (proof : Native64ResultSortGate x!14 #3 #2 #1 #0) => Sort 1) Sort 0 (Native64SortGateB.0.3766726852 ((fun (salt : Nat) => x!14) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => x!14) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => x!14) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => x!14) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) x!15