Lean Kernel Arena / eink0rn / corner-cases/vanishing-occurrence

Checker "eink0rn" on test "corner-cases/vanishing-occurrence"

Checker: eink0rn · Version: 1.1.6 · 📄 Declaration · 🔗 Source

Test: corner-cases/vanishing-occurrence · Expected: 🤷 either · Size: 7.2 KB · Lines: 110 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Result: ✋ rejected · exit code 1 · wall time: 9.73 ms · instructions: 8.7 M · max rss memory: 11.7 MB · run 2026-11-01 13:08:41 UTC

stdout:
REJECT
stderr:
VanishPos: VanishPos is declared with isRec = true, but the kernel derives false