Checker "tenet-jvm" on test "bugs/nested-name-capture"
Checker: tenet-jvm · Version: 0.1.3 · 📄 Declaration · 🔗 Source
Test: bugs/nested-name-capture · Expected: ✋ reject · Size: 26.1 KB · Lines: 433 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 79.9 ms · instructions: 869.4 M · max rss memory: 66.2 MB · run 2026-10-27 21:10:25 UTC
stdout:
REJECTED inductive Shadow: recursor rule for Shadow.node has the wrong right-hand side
expected: (fun motive_1 : (? t : Shadow, Sort(u)) => (fun motive_2 : (? t : (Cov Shadow), Sort(u)) => (fun minor : (#1 Shadow.base) => (fun minor : (? a._@._internal._hyg.0 : (Cov Shadow), (? a_ih._@._internal._hyg.0 : (#2 #0), (#4 (Shadow.node #1)))) => (fun minor : (? a._@._internal._hyg.0 : (? a._@._internal._hyg.0 : U, Shadow), (? a_ih._@._internal._hyg.0 : (? a._@._internal._hyg.0 : U, (#5 (#1 #0))), (#4 (Cov.mk Shadow #1)))) => (fun a._@._internal._hyg.0 : (Cov Shadow) => (#2 #0 (Shadow.rec_1.{[u]} #5 #4 #3 #2 #1 #0))))))))
exported: (fun motive_1 : (? t : Shadow, Sort(u)) => (fun motive_2 : (? t : (Cov Shadow), Sort(u)) => (fun base : (#1 Shadow.base) => (fun node : (? a._@._internal._hyg.0 : (Cov Shadow), (? a_ih._@._internal._hyg.0 : (#2 #0), (#4 (Shadow.node #1)))) => (fun mk : (? a._@._internal._hyg.0 : (? a._@._internal._hyg.0 : U, Shadow), (? a_ih._@._internal._hyg.0 : (? a._@._internal._hyg.0 : U, (#5 (#1 #0))), (#4 (Cov.mk Shadow #1)))) => (fun a._@._internal._hyg.0 : (Cov Shadow) => (#2 #0 (_nested.Cov_1.rec.{[u]} #5 #4 #3 #2 #1 (_nested.Cov_1.mk #0.1)))))))))
lean 4.34.1, export format 3.1.0, 433 lines
checked 30 constants ({DEF=9}) and 7 inductive blocks in 0.04s
axioms declared: none
1 declaration(s) rejected