Lean Kernel Arena / logos-kernel / corner-cases/alg-conv-trans-acc

Checker: logos-kernel · Version: 1e6ad5b · 📄 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: 3.93 ms · instructions: 5.6 M · max rss memory: 4.9 MB · run 2026-11-08 11:08:24 UTC

stderr:

rejected: declaration 'trans': declaration type mismatch
  the value has type
    (Acc Nat (…) (…)) → Eq.refl Bool (f (OfNat.ofNat Nat 1 (instOfNatNat 1)) #0)
  but is declared with type
    (Acc Nat (…) (…)) → Eq Bool (f (OfNat.ofNat Nat 1 (instOfNatNat 1)) #0) (f (OfNat.ofNat Nat 0 (instOfNatNat 0)) (Acc.inv Nat (fun (x0 : Nat) => fun (x1 : Nat) => LT.lt Nat instLTNat x0 x1) (OfNat.ofNat Nat 1 (instOfNatNat 1)) (OfNat.ofNat Nat 0 (instOfNatNat 0)) #0 (Nat.lt_succ_self (OfNat.ofNat Nat 0 (instOfNatNat 0)))))