Function compare_level

crates/compile/src/compile.rs:2385–2436

Compare two universe levels structurally, using level parameter position (not name) for `Param` comparisons.

(
  x: &Level,
  y: &Level,
  x_ctx: &[Name],
  y_ctx: &[Name],
)

  let value_root = *cache.arena_roots.last().expect("missing value arena root");

  // Take arena, surgery sharing, and level-spelling channels (canonicity
  // §10.6), clear for next constant
  let arena = std::mem::take(&mut cache.arena);
  let surgery_sharing = std::mem::take(&mut cache.surgery_sharing);
  let meta_univs: Vec<Arc<Univ>> =
    std::mem::take(&mut cache.meta_univs).into_iter().collect();
  let univ_patches = std::mem::take(&mut cache.univ_patches);
  cache.arena_roots.clear();
  cache.exprs.clear();

  let name_addr = compile_name(&def.name, stt);
  let lvl_addrs: Vec<Address> =
    univ_params.iter().map(|n| compile_name(n, stt)).collect();
  let all_addrs: Vec<Address> =
    def.all.iter().map(|n| compile_name(n, stt)).collect();
  let ctx_addrs: Vec<Address> = ctx_addrs.to_vec();

  let data = Definition {
    kind: def.kind,
    safety: def.safety,
    lvls: def.level_params.len() as u64,
    typ,
    value,
  };

  let mut meta = ConstantMeta::new(ConstantMetaInfo::Def {
    name: name_addr,
    lvls: lvl_addrs,
    all: all_addrs,
    ctx: ctx_addrs,
    arena,
    type_root,
    value_root,
  });
  meta.meta_sharing = surgery_sharing;
  meta.meta_univs = meta_univs;
  meta.univ_patches = univ_patches;
  stt.def_hints.insert(def.name.clone(), def.hints);

  Ok((data, meta))
}

/// Compile a RecursorRule.
fn compile_recursor_rule(
  rule: &LeanRecursorRule,
  univ_params: &[Name],
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
) -> Result<(RecursorRule, Address), CompileError> {
  let rhs = compile_expr(&rule.rhs, univ_params, mut_ctx, cache, stt)?;
  let ctor_addr = compile_name(&rule.ctor, stt);
  let fields = nat_to_u64(&rule.n_fields, "n_fields too large")?;

  Ok((RecursorRule { fields, rhs }, ctor_addr))