Function level_alpha_eq

crates/compile/src/congruence.rs:41–43

Check that two Lean levels are equal modulo the same simplifications `Level::max_smart` / `Level::imax_smart` perform. Why normalize: `aux_gen::expr_utils::subst_level` routes through the smart constructors so substituted levels match the form the kernel produces post-ingress (see commit `ec95312` "Align nested-aux canonical order"). Lean's own `Level.instantiateParams` keeps the un-simplified fa

(a: &Level, b: &Level)

/// only introduce drift. See the "Use raw Level::succ" comment that lived
/// in `expr_utils::subst_level` prior to `ec95312`.
pub fn level_alpha_eq(a: &Level, b: &Level) -> Result<(), String> {
  level_alpha_eq_struct(&normalize_level(a), &normalize_level(b))
}

/// Normalize a level by applying `Level::max_smart` / `Level::imax_smart`
/// bottom-up. Idempotent. `Succ` is left raw (see [`level_alpha_eq`]).