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

Checker: eink0rn · Version: 1.1.6 · 📄 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: 12.6 ms · instructions: 9.9 M · max rss memory: 12.3 MB · run 2026-10-24 16:43:29 UTC

stdout:

REJECT

stderr:

left: type mismatch:
  term     fun (P : Sort 0) => fun (r : (a._@._internal._hyg.0 : #0) -> (a._@._internal._hyg.0 : #1) -> Sort 0) => fun (α : Sort 1) => fun (f : (a : #2) -> #1) => fun (h : (x : #3) -> (y : #4) -> (a._@._internal._hyg.0 : #4 #1 #0) -> Eq.{1} #4 (#3 #2) (#3 #1)) => fun (q : Quot.{0} #4 #3) => fun (z : #5) => Eq.refl.{1} #4 (Quot.lift.{0, 1} #6 #5 #4 #3 #2 #1)
  has type (P : Sort 0) -> (r : (a._@._internal._hyg.0 : #0) -> (a._@._internal._hyg.0 : #1) -> Sort 0) -> (α : Sort 1) -> (f : (a : #2) -> #1) -> (h : (x : #3) -> (y : #4) -> (a._@._internal._hyg.0 : #4 #1 #0) -> Eq.{1} #4 (#3 #2) (#3 #1)) -> (q : Quot.{0} #4 #3) -> (z : #5) -> Eq.{1} #4 (Quot.lift.{0, 1} #6 #5 #4 #3 #2 #1) (Quot.lift.{0, 1} #6 #5 #4 #3 #2 #1)
  expected (P : Sort 0) -> (r : (a._@._internal._hyg.0 : #0) -> (a._@._internal._hyg.0 : #1) -> Sort 0) -> (α : Sort 1) -> (f : (a : #2) -> #1) -> (h : (x : #3) -> (y : #4) -> (a._@._internal._hyg.0 : #4 #1 #0) -> Eq.{1} #4 (#3 #2) (#3 #1)) -> (q : Quot.{0} #4 #3) -> (z : #5) -> Eq.{1} #4 (Quot.lift.{0, 1} #6 #5 #4 #3 #2 #1) (Quot.lift.{0, 1} #6 #5 #4 #3 #2 (Quot.mk.{0} #6 #5 #0))