Function level_param_matches

crates/kernel/src/congruence.rs:452–459

()

  #[test]
  fn level_param_matches() {
    // Lean Param has a name; zero Param has a positional index. Without a
    // level_params list the check must pass (see module comment).
    let r = empty_resolver();
    let ll = LL::param(mk_name("u"));
    let lu = KUniv::<Anon>::param(0, ());
    level_congruent(&ll, &lu, &r).unwrap();
  }

  #[test]
  fn level_zero_vs_succ_fails() {