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

Checker: logos-kernel · Version: 1e6ad5b · 📄 Declaration · 🔗 Source

Test: corner-cases/alg-conv-trans-quot-left · Expected: 🤷 either · Size: 8.6 KB · Lines: 173 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Result: ✋ rejected · exit code 1 · wall time: 2.68 ms · instructions: 2.8 M · max rss memory: 4.6 MB · run 2026-11-08 11:08:24 UTC

stderr:

rejected: declaration 'left': declaration type mismatch
  the value has type
    (Sort LevelId(0)) → fun (x0 : (x0 : #0) → #1 → Prop) => fun (x1 : Sort (1)) => fun (x2 : (x2 : #2) → x1) => fun (x3 : (x3 : #3) → (x4 : #4) → (x5 : x0 x3 x4) → Eq x1 (x2 x3) (x2 x4)) => fun (x4 : Quot #4 x0) => fun (x5 : #5) => Eq.refl x1 (Quot.lift #6 x0 x1 x2 x3 x4)
  but is declared with type
    (Sort LevelId(0)) → (x0 : (x0 : #0) → #1 → Prop) → (x1 : Sort (1)) → (x2 : (x2 : #2) → x1) → (x3 : (x3 : #3) → (x4 : #4) → (x5 : x0 x3 x4) → Eq x1 (x2 x3) (x2 x4)) → (x4 : Quot #4 x0) → (x5 : #5) → Eq x1 (Quot.lift #6 x0 x1 x2 x3 x4) (Quot.lift #6 x0 x1 x2 x3 (Quot.mk #6 x0 x5))