Checker "rpylean" on test "bugs/forged-quot-ind"
Checker: rpylean · Version: v2026.9.1 · 📄 Declaration · 🔗 Source
Test: bugs/forged-quot-ind · Expected: ✋ reject · Size: 11.6 KB · Lines: 204 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 46.8 ms · instructions: 4.0 M · max rss memory: 4.2 MB · run 2026-10-27 21:10:12 UTC
stderr:
Quot.ind : {A : Sort u} →
{r : ∀ (a a : A), Prop} → {B : ∀ (a : Quot A r), Prop} → ((a : A) → B (Quot.mk A r a)) → (q : Quot A r) → B q
unknown declaration Quot
summary: 16/16 decls checked, peak 32 MB, allocated 0 MB, heartbeats 0
checked in 0.000514s