Function compare_ctor_inner

crates/compile/src/compile.rs:2618–2643

Compare two constructors by level params, cidx, params, fields, then type.

(
  x: &ConstructorVal,
  y: &ConstructorVal,
  mut_ctx: &MutCtx,
  stt: &CompileState,
)

    type_root,
  });
  meta.meta_sharing = indc_surgery_sharing;
  meta.meta_univs = indc_meta_univs;
  meta.univ_patches = indc_univ_patches;

  Ok((data, meta, ctor_const_metas))
}

/// Compile an Axiom.
fn compile_axiom(
  val: &AxiomVal,
  cache: &mut BlockCache,
  stt: &CompileState,
) -> Result<(Axiom, ConstantMeta), CompileError> {
  cache.compiling = Some(val.cnst.name.clone());
  let univ_params = &val.cnst.level_params;

  let typ =
    compile_expr(&val.cnst.typ, univ_params, &MutCtx::default(), cache, stt)?;
  let type_root =
    *cache.arena_roots.last().expect("missing axiom type arena root");

  // Drain surgery sharing onto this axiom's meta. Axioms can reference
  // alpha-collapsed auxiliaries in their type; any collapsed args must
  // stay with this axiom rather than leak to the next constant. Same for
  // the level-spelling channels (canonicity §10.6).
  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();