Function norm_add_const

crates/kernel/src/level.rs:345–351

(s: &mut NormLevel, k: u64, path: &[u64])

/// `NormLevel.addNode v k path'` (`refs/lean4lean/Lean4Lean/Level.lean:92`);
/// `k` must be the current succ-accumulator from `normalize_aux`.
///
/// An earlier port of this function dropped `k` and always inserted
/// `(idx, 0)`, which silently mis-normalized `Succ^n(imax(u, Param v))`
/// shapes for `n > 0`. Keep the `k` parameter.
fn norm_add_node(s: &mut NormLevel, idx: u64, k: u64, path: &[u64]) {
  s.entry(path.to_vec()).or_default().add_var(idx, k);
}

fn norm_add_const(s: &mut NormLevel, k: u64, path: &[u64]) {
  if k == 0 || (k == 1 && !path.is_empty()) {