Function subsume_vars

crates/kernel/src/level.rs:506–533

Subsumption (Phase 2)

(xs: &[VarNode], ys: &[VarNode])

    }
  } else {
    // All UnivData variants for `b` are covered above.
    unreachable!(
      "normalize_imax_dispatch: all UnivData variants for b should be covered"
    );
  }
}

// Subsumption (Phase 2)
fn subsume_vars(xs: &[VarNode], ys: &[VarNode]) -> Vec<VarNode> {
  let mut result = Vec::new();
  let mut xi = 0;
  let mut yi = 0;
  while xi < xs.len() {
    if yi >= ys.len() {
      result.extend_from_slice(&xs[xi..]);
      break;
    }
    match xs[xi].idx.cmp(&ys[yi].idx) {
      std::cmp::Ordering::Less => {
        result.push(xs[xi].clone());
        xi += 1;
      },
      std::cmp::Ordering::Equal => {
        if xs[xi].offset > ys[yi].offset {
          result.push(xs[xi].clone());
        }
        xi += 1;
        yi += 1;
      },
      std::cmp::Ordering::Greater => {
        yi += 1;