Checker "eink0rn" on test "bugs/rec-missing-ih"
Checker: eink0rn · Version: 1.1.6 · 📄 Declaration · 🔗 Source
Test: bugs/rec-missing-ih · Expected: ✋ reject · Size: 289.6 KB · Lines: 5.5 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 16.8 ms · instructions: 75.4 M · max rss memory: 29.9 MB · run 2026-10-24 16:43:29 UTC
stdout:
REJECT
stderr:
Native64TwoHashOwner: constructor Native64TwoHashOwner.step of Native64TwoHashOwner: recursive field must be headed by Native64TwoHashOwner, got Native64TwoHashGate.rec.{2} x!15 (fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (proof : Native64TwoHashGate x!15 #3 #2 #1 #0) => Sort 1) Native64TwoHashOwner (Native64TwoHashB.0.2525080234 ((fun (salt : Nat) => x!15) (OfNat.ofNat.{0} Nat 101831 (instOfNatNat 101831)))) (Native64TwoHashA.0.572478232 ((fun (salt : Nat) => x!15) (OfNat.ofNat.{0} Nat 101831 (instOfNatNat 101831)))) (Native64TwoHashA.0.572478232 ((fun (salt : Nat) => x!15) (OfNat.ofNat.{0} Nat 101831 (instOfNatNat 101831)))) (Native64TwoHashA.0.572478232 ((fun (salt : Nat) => x!15) (OfNat.ofNat.{0} Nat 101831 (instOfNatNat 101831)))) x!17