Checker "tenet" on test "corner-cases/alg-conv-trans-acc"
Checker: tenet · Version: 0.11.3 · 📄 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: 138 ms · instructions: 917.6 M · max rss memory: 47.1 MB · run 2026-10-24 16:42:18 UTC
stdout:
FAIL thm trans (0.00s)
declaration type mismatch for 'trans'
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 x1.«_@».Test.1043551373._hygCtx._hyg.6 x2.«_@».Test.1043551373._hygCtx._hyg.6) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))), Eq.{1} Bool (f (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) a) (f (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (Acc.inv.{1} Nat (fun (x1.«_@».Test.1043551373._hygCtx._hyg.6 : Nat) => fun (x2.«_@».Test.1043551373._hygCtx._hyg.6 : Nat) => LT.lt.{0} Nat instLTNat x1.«_@».Test.1043551373._hygCtx._hyg.6 x2.«_@».Test.1043551373._hygCtx._hyg.6) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) a (Nat.lt_succ_self (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))))
inferred: ∀ (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 x1.«_@».Test.1043551373._hygCtx._hyg.6 x2.«_@».Test.1043551373._hygCtx._hyg.6) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))), Eq.{1} Bool (f (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) a) (f (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) a)
FAILED: 39 checked, 1 failed, 0 skipped, 67 constants, 0.1s, 4 jobs