Function compile_single_def

crates/compile/src/compile.rs:3228–3301

Helper: compile a single definition/theorem/opaque (non-mutual case). When `aux` is false (ephemeral compilation for metadata capture), skip storing the Ixon blob, Named entry, and block stats.

(
    name: &Name,
    def: &Def,
    cache: &mut BlockCache,
    stt: &CompileState,
    aux: bool,
  )

    (MutConst::Defn(x), MutConst::Defn(y)) => compare_defn(x, y, mut_ctx, stt)?,
    (MutConst::Indc(x), MutConst::Indc(y)) => {
      compare_indc(x, y, mut_ctx, cache, stt)?
    },
    (MutConst::Recr(x), MutConst::Recr(y)) => compare_recr(x, y, mut_ctx, stt)?,
    _ => SOrd::cmp(&mut_const_kind(x), &mut_const_kind(y)),
  };
  if so.strong {
    cache.cmps.insert(key, so.ordering);
  }
  Ok(if reversed { so.ordering.reverse() } else { so.ordering })
}

/// Check if two mutual constants are structurally equal.
pub fn eq_const(
  x: &MutConst,
  y: &MutConst,
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
) -> Result<bool, CompileError> {
  let ordering = compare_const(x, y, mut_ctx, cache, stt)?;
  Ok(ordering == Ordering::Equal)
}

/// Group consecutive equal elements in a sorted slice. Assumes the input
/// is already sorted by the same relation used for equality testing.
pub fn group_by<T, F>(
  items: Vec<&T>,
  mut eq: F,
) -> Result<Vec<Vec<&T>>, CompileError>
where
  F: FnMut(&T, &T) -> Result<bool, CompileError>,
{
  let mut groups = Vec::new();
  let mut current: Vec<&T> = Vec::new();
  for item in items {
    if let Some(last) = current.last() {
      if eq(last, item)? {
        current.push(item);
      } else {
        groups.push(std::mem::replace(&mut current, vec![item]));
      }
    } else {
      current.push(item);
    }
  }
  if !current.is_empty() {
    groups.push(current);
  }
  Ok(groups)
}

/// Merge two sorted sequences of mutual constants into one sorted sequence.
pub fn merge<'a>(
  left: Vec<&'a MutConst>,
  right: Vec<&'a MutConst>,
  ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,