Function level_succ_inner_propagates_error

crates/kernel/src/congruence.rs:484–492

()

  #[test]
  fn level_succ_inner_propagates_error() {
    let r = empty_resolver();
    // Succ(Zero) vs Succ(Succ(Zero)) — outer shape matches, inner differs.
    let ll = LL::succ(LL::zero());
    let lu = KUniv::<Anon>::succ(KUniv::succ(KUniv::zero()));
    let e = level_congruent(&ll, &lu, &r).unwrap_err();
    assert!(e.contains("Zero"));
    assert!(e.contains("Succ"));
  }

  // ---- expr_congruent ----