Checker "tenet" on test "bugs/ctor-num-fields"
Checker: tenet · Version: 0.11.3 · 📄 Declaration · 🔗 Source
Test: bugs/ctor-num-fields · Expected: ✋ reject · Size: 34.1 KB · Lines: 622 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Result: ✋ rejected · exit code 1 · wall time: 140 ms · instructions: 841.2 M · max rss memory: 45.4 MB · run 2026-10-24 16:42:18 UTC
stdout:
FAIL inductive _private.Test.0.S (0.00s)
'_private.Test.0.S.mk': exported numFields does not match the kernel's
exported: 0
kernel: 1
FAILED: 24 checked, 1 failed, 0 skipped, 40 constants, 0.1s, 4 jobs