Function compare_indc

crates/compile/src/compile.rs:2678–2729

Compare two inductives by derived flags, params, indices, constructor count, type, then constructors. Includes `is_rec` and `is_unsafe` to prevent alpha-collapse from merging inductives whose derived properties differ — a mismatch in `is_rec` would cause the collapsed representative to silently omit `.brecOn` for aliases that need it (or generate it for aliases that shouldn't have it).

(
  x: &Ind,
  y: &Ind,
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
)

) -> Result<(Quotient, 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 quot type arena root");

  // Drain surgery sharing onto this quotient's meta — same reasoning as
  // in compile_axiom / compile_recursor / etc.: keep collapsed args
  // attached to the constant whose compilation produced them. 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();
  let univ_patches = std::mem::take(&mut cache.univ_patches);
  cache.arena_roots.clear();
  cache.exprs.clear();

  let name_addr = compile_name(&val.cnst.name, stt);
  let lvl_addrs: Vec<Address> =
    univ_params.iter().map(|n| compile_name(n, stt)).collect();

  let data = Quotient { kind: val.kind, lvls: univ_params.len() as u64, typ };

  let mut meta = ConstantMeta::new(ConstantMetaInfo::Quot {
    name: name_addr,
    lvls: lvl_addrs,
    arena,
    type_root,
  });
  meta.meta_sharing = surgery_sharing;
  meta.meta_univs = meta_univs;
  meta.univ_patches = univ_patches;

  Ok((data, meta))
}

// ===========================================================================
// Mutual block compilation
// ===========================================================================

/// Result of compiling a mutual block.
pub struct CompiledMutualBlock {
  /// The compiled Constant
  pub constant: Constant,
  /// Content-addressed hash
  pub addr: Address,
  /// Hash-consed size (theoretical minimum with perfect DAG sharing)
  pub hash_consed_size: usize,
  /// Serialized size (actual bytes)
  pub serialized_size: usize,
}

/// Compile a mutual block with block-level sharing.