Checker "mathgraph" on test "corner-cases/nested-redex-aux"
Checker: mathgraph · Version: flash · 📄 Declaration · 🔗 Source
Test: corner-cases/nested-redex-aux · Expected: 🤷 either · Size: 43.0 KB · Lines: 755 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Result: ✋ rejected · exit code 1 · wall time: 6.50 ms · instructions: 6.1 M · max rss memory: 39.8 MB · run 2026-11-01 13:15:45 UTC
stderr:
thread 'thread_0' (5353) panicked at src/inductive.rs:383:9:
assertion `left == right` failed: imported inductive block contains an underived recursor
left: {NamePtr(0x2f8ec331bb8), NamePtr(0x2f8ec330ae8), NamePtr(0x2f8ec330f40)}
right: {NamePtr(0x2f8ec331bb8), NamePtr(0x2f8ec330f40)}
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread 'main' (5352) panicked at src/tc.rs:213:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }