Checker "ocaml4lean" on test "bugs/proj-of-stuck-prop"
Checker: ocaml4lean · Version: 3753af7 · 📄 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: 21.3 ms · instructions: 177.8 M · max rss memory: 30.7 MB · run 2026-11-08 11:05:32 UTC
stdout:
rejected (3 failing blocks): type expected: (Native64ResultSortGate.rec.{2} _x358 (fun _ : Bool => (fun _ : Bool => (fun _ : Bool => (fun _ : Bool => (fun _ : (Native64ResultSortGate _x358 #3 #2 #1 #0) => Sort 1))))) Sort 0 (Native64SortGateB.0.3766726852 ((fun _ : Nat => _x358) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64So...
stderr:
error in block 106 (Native64ResultSort.asProp): application type mismatch: argument (Native64ResultSortOwner _x461 _x463) has type (Native64ResultSortGate.rec.{2} _x461 (fun _ : Bool => (fun _ : Bool => (fun _ : Bool => (fun _ : Bool => (fun _ : (Native64ResultSortGate _x461 #3 #2 #1 #0) => Sort 1))))) Sort 0 (Native64SortGateB.0.3766726852 ((fun _ : Nat => _x461) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64So... but is expected to have type Sort 0
error in block 105 (Native64ResultSortOwner, Native64ResultSortOwner.mk, Native64ResultSortOwner.rec): type expected: (Native64ResultSortGate.rec.{2} _x358 (fun _ : Bool => (fun _ : Bool => (fun _ : Bool => (fun _ : Bool => (fun _ : (Native64ResultSortGate _x358 #3 #2 #1 #0) => Sort 1))))) Sort 0 (Native64SortGateB.0.3766726852 ((fun _ : Nat => _x358) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64So...
error in block 116 (Native64ResultSortLeak.observe): type expected: (Native64ResultSortGate.rec.{2} Bool.false (fun _ : Bool => (fun _ : Bool => (fun _ : Bool => (fun _ : Bool => (fun _ : (Native64ResultSortGate Bool.false #3 #2 #1 #0) => Sort 1))))) Sort 0 (Native64SortGateB.0.3766726852 ((fun _ : Nat => Bool.false) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)...