Lean Kernel Arena / nanobruijn / bugs/unit-rec-rule

Checker: nanobruijn · Version: 7a04996 · 📄 Declaration · 🔗 Source

Test: bugs/unit-rec-rule · Expected: ✋ reject · Size: 3.0 KB · Lines: 54 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration

Result: ✋ rejected · exit code 1 · wall time: 3.74 ms · instructions: 3.9 M · max rss memory: 5.5 MB · run 2026-10-27 12:14:06 UTC

stderr:

ExprPtr parse: 30 parser entries → 28 DAG entries, 1 OSNF-shifted, 27 live after compaction, 0 cores with bvar indices >= 64 (0 tail words)
  assert_def_eq FAILED at depth 0:
    u = Lam(Pi(C(PUnit)+65535,Sort(ExportFile@2)+65535)+65535,Lam(App(V0+0,C(unit)+65535)+0,C(unit)+65535)+0) (shift=65535 nlbv=0)
    v = Lam(Pi(C(PUnit)+65535,Sort(ExportFile@2)+65535)+65535,Lam(App(V0+0,C(unit)+65535)+0,V0+0)+0) (shift=65535 nlbv=0)
    DIFF Lam at depth 0
        DIFF Lam at depth 1
            SHIFT DIFF: shift=65535 vs shift=0
            LEAF DIFF at depth 2: C(unit) vs V0

thread 'thread_0' (4818) panicked at src/tc.rs:1423:13:
assert_def_eq failed
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
  assert_def_eq FAILED at depth 0:
    u = App(App(App(C(rec)+65535,Lam(C(PUnit)+65535,Sort(ExportFile@0)+65535)+65535)+65535,C(EmptyProp)+65535)+65535,C(unit)+65535) (shift=65535 nlbv=0)
    v = C(EmptyProp) (shift=65535 nlbv=0)
    LEAF DIFF at depth 0: App(App(App(C(rec)+65535,Lam(C(PUnit)+65535,Sort(ExportFile@0)+65535)+65535)+65535,C(EmptyProp)+65535)+65535,C(unit)+65535) vs C(EmptyProp)

thread 'thread_2' (4820) panicked at src/tc.rs:1423:13:
assert_def_eq failed

thread 'main-worker' (4817) panicked at src/tc.rs:324:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }
  assert_def_eq FAILED at depth 0:
    u = C(PUnit) (shift=65535 nlbv=0)
    v = App(App(App(C(rec)+65535,Lam(C(PUnit)+65535,Sort(ExportFile@0)+65535)+65535)+65535,C(EmptyProp)+65535)+65535,C(unit)+65535) (shift=65535 nlbv=0)
    LEAF DIFF at depth 0: C(PUnit) vs App(App(App(C(rec)+65535,Lam(C(PUnit)+65535,Sort(ExportFile@0)+65535)+65535)+65535,C(EmptyProp)+65535)+65535,C(unit)+65535)

thread 'thread_3' (4821) panicked at src/tc.rs:1423:13:
assert_def_eq failed

thread 'main' (4816) panicked at src/main.rs:11:20:
called `Result::unwrap()` on an `Err` value: Any { .. }