Function norm_add_node

crates/kernel/src/level.rs:341–343

Insert `(idx, k)` into the var list at `path`, taking the max of offsets when `idx` is already present. Mirrors Lean4Lean's `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))` shap

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

}

/// Insert `(idx, k)` into the var list at `path`, taking the max of offsets
/// when `idx` is already present. Mirrors Lean4Lean's
/// `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