Lean Kernel Arena / tenet / corner-cases/eta-struct-major-and-no-whnf

Checker "tenet" on test "corner-cases/eta-struct-major-and-no-whnf"

Checker: tenet · Version: 0.11.3 · 📄 Declaration · 🔗 Source

Test: corner-cases/eta-struct-major-and-no-whnf · Expected: 🤷 either · Size: 24.0 KB · Lines: 421 · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 60.0 s · 📄 Declaration · 🔗 Source

Result: ✋ rejected · exit code 1 · wall time: 13.8 s · instructions: 231.1 G · max rss memory: 549.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL thm andMajorNoWhnf (13.66s)
    deterministic timeout: more than 100000000 definition unfoldings while checking one declaration (TypeChecker.MaxUnfolds)
FAILED: 17 checked, 1 failed, 0 skipped, 31 constants, 13.7s, 4 jobs