Function mk_name

crates/kernel/src/level.rs:716–722

(s: &str)

}

/// Normalize a universe level to Géran's canonical form.
fn normalize_level<M: KernelMode>(l: &KUniv<M>) -> NormLevel {
  let mut acc = NormLevel::new();
  acc.insert(Vec::new(), Node::default());
  normalize_aux(l, &[], 0, &mut acc);
  subsumption(&mut acc);
  acc
}

/// Semantic universe equality: `u ≡ v` for all parameter assignments.