Lean Kernel Arena / tenet / bugs/proj-of-stuck-prop

Checker "tenet" on test "bugs/proj-of-stuck-prop"

Checker: tenet · Version: 0.11.3 · 📄 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: 146 ms · instructions: 1.1 G · max rss memory: 52.6 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive Native64ResultSortOwner (0.01s)
    type expected, but got
      Native64ResultSortGate.rec.{2} _fvar.1099511628480 (fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (proof : Native64ResultSortGate _fvar.1099511628480 index index index index) => Type) Prop (Native64SortGateB.0.3766726852 ((fun (salt : Nat) => _fvar.1099511628480) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => _fvar.1099511628480) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => _fvar.1099511628480) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => _fvar.1099511628480) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) _fvar.1099511628481
    of type
      Native64ResultSortGate.rec.{2} _fvar.1099511628480 (fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (proof : Native64ResultSortGate _fvar.1099511628480 index index index index) => Type) Prop (Native64SortGateB.0.3766726852 ((fun (salt : Nat) => _fvar.1099511628480) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => _fvar.1099511628480) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => _fvar.1099511628480) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => _fvar.1099511628480) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) _fvar.1099511628481
FAIL def Native64ResultSort.asProp (0.01s)
    application type mismatch in
      id.{1} Prop (Native64ResultSortOwner x h)
    argument has type
      Native64ResultSortGate.rec.{2} x (fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (proof : Native64ResultSortGate x index index index index) => Type) Prop (Native64SortGateB.0.3766726852 ((fun (salt : Nat) => x) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => x) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => x) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => x) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) h
    but function has type
      Prop → Prop
FAIL def Native64ResultSortLeak.observe (0.00s)
    type expected, but got
      Native64ResultSortGate.rec.{2} Bool.false (fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (proof : Native64ResultSortGate Bool.false index index index index) => Type) Prop (Native64SortGateB.0.3766726852 ((fun (salt : Nat) => Bool.false) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => Bool.false) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => Bool.false) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => Bool.false) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) Native64ResultSort.closedGate
    of type
      Native64ResultSortGate.rec.{2} Bool.false (fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (index : Bool) => fun (proof : Native64ResultSortGate Bool.false index index index index) => Type) Prop (Native64SortGateB.0.3766726852 ((fun (salt : Nat) => Bool.false) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => Bool.false) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => Bool.false) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) (Native64SortGateA.1.2023879994 ((fun (salt : Nat) => Bool.false) (OfNat.ofNat.{0} Nat 125330 (instOfNatNat 125330)))) Native64ResultSort.closedGate
FAILED: 117 checked, 3 failed, 0 skipped, 164 constants, 0.1s, 4 jobs