Checker "tenet-jvm" on test "corner-cases/large-elim-maybe-prop"
Checker: tenet-jvm · Version: 0.1.3 · 📄 Declaration · 🔗 Source
Test: corner-cases/large-elim-maybe-prop · Expected: 🤷 either · Size: 3.1 KB · Lines: 55 · lean4export: 3.1.0 · Lean: 4.35.0 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 93.0 ms · instructions: 632.4 M · max rss memory: 65.0 MB · run 2026-11-01 13:26:53 UTC
stdout:
REJECTED inductive MaybePropBox: recursor MaybePropBox.rec has the wrong type
expected: (? ? : Sort(u), (? motive : (? t : (MaybePropBox.{[u]} #0), Sort(0)), (? mk : (? x : #1, (#1 (MaybePropBox.mk.{[u]} #2 #0))), (? t : (MaybePropBox.{[u]} #2), (#2 #0)))))
exported: (? ? : Sort(u), (? motive : (? t : (MaybePropBox.{[u]} #0), Sort(u_1)), (? mk : (? x : #1, (#1 (MaybePropBox.mk.{[u]} #2 #0))), (? t : (MaybePropBox.{[u]} #2), (#2 #0)))))
lean 4.35.0, export format 3.1.0, 55 lines
checked 0 constants ({}) and 0 inductive blocks in 0.03s
axioms declared: none
1 declaration(s) rejected