Function level_congruent

crates/kernel/src/congruence.rs:34–59

Check that a Lean-side Level matches a zero Univ structurally.

(
  lean_lvl: &lean::Level,
  zero_univ: &KUniv<Anon>,
  _nr: &NameResolver,
)

/// Check that a Lean-side Level matches a zero Univ structurally.
pub fn level_congruent(
  lean_lvl: &lean::Level,
  zero_univ: &KUniv<Anon>,
  _nr: &NameResolver,
) -> Result<(), String> {
  use lean::LevelData as LD;
  match (lean_lvl.as_data(), zero_univ.data()) {
    (LD::Zero(_), UnivData::Zero(_)) => Ok(()),
    (LD::Succ(a, _), UnivData::Succ(b, _)) => level_congruent(a, b, _nr),
    (LD::Max(a1, a2, _), UnivData::Max(b1, b2, _))
    | (LD::Imax(a1, a2, _), UnivData::IMax(b1, b2, _)) => {
      level_congruent(a1, b1, _nr)?;
      level_congruent(a2, b2, _nr)
    },
    (LD::Param(_, _), UnivData::Param(_, _, _)) => {
      // Lean uses named params, zero uses positional indices.
      // Can't check correspondence without level_params list.
      Ok(())
    },
    _ => Err(format!(
      "level mismatch: lean={} vs zero={}",
      lean_lvl_tag(lean_lvl),
      zero_univ_tag(zero_univ),
    )),
  }
}

/// Check that a Lean-side Expr matches a zero Expr<Anon> structurally.
pub fn expr_congruent(