Function compare_expr

crates/compile/src/compile.rs:2464–2572

Compare two Lean expressions structurally for canonical ordering. Strips `Mdata` wrappers, compares by constructor tag, then recurses into subexpressions. Constants are compared by address (or mutual index).

(
  x: &LeanExpr,
  y: &LeanExpr,
  mut_ctx: &MutCtx,
  x_lvls: &[Name],
  y_lvls: &[Name],
  stt: &CompileState,
)

    rules,
  };

  let all_addrs: Vec<Address> =
    rec.all.iter().map(|n| compile_name(n, stt)).collect();
  let ctx_addrs: Vec<Address> =
    ctx_to_all(mut_ctx).iter().map(|n| compile_name(n, stt)).collect();

  let mut meta = ConstantMeta::new(ConstantMetaInfo::Rec {
    name: name_addr,
    lvls: lvl_addrs,
    rules: rule_addrs,
    all: all_addrs,
    ctx: ctx_addrs,
    arena,
    type_root,
    rule_roots,
  });
  meta.meta_sharing = surgery_sharing;
  meta.meta_univs = meta_univs;
  meta.univ_patches = univ_patches;

  Ok((data, meta))
}

/// Compile a Constructor.
/// Each constructor gets its own arena.
fn compile_constructor(
  ctor: &ConstructorVal,
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
) -> Result<(Constructor, ConstantMeta), CompileError> {
  cache.compiling = Some(ctor.cnst.name.clone());
  let univ_params = &ctor.cnst.level_params;

  let typ = compile_expr(&ctor.cnst.typ, univ_params, mut_ctx, cache, stt)?;
  let type_root =
    *cache.arena_roots.last().expect("missing ctor type arena root");

  // Take arena and surgery sharing for this constructor. A ctor's type
  // may contain surgered call-sites when the ctor's field types reference
  // alpha-collapsed auxiliaries, so drain here to attach to THIS ctor's
  // meta rather than leaking into whichever constant comes next.
  // Level-spelling channels (canonicity §10.6) drain on the same
  // boundary — the decompiler's ctor-scoped window installs them per
  // constructor.
  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(&ctor.cnst.name, stt);
  let lvl_addrs: Vec<Address> =
    univ_params.iter().map(|n| compile_name(n, stt)).collect();
  let induct_addr = compile_name(&ctor.induct, stt);