Function group_by

crates/compile/src/compile.rs:2850–2874

Group consecutive equal elements in a sorted slice. Assumes the input is already sorted by the same relation used for equality testing.

(
  items: Vec<&T>,
  mut eq: F,
)

  stt: &CompileState,
  caller: &'static str,
) -> Result<SOrd, CompileError> {
  match (stt.resolve_addr(x), stt.resolve_addr(y)) {
    (Some(xa), Some(ya)) => Ok(SOrd::cmp(&xa, &ya)),
    (None, _) => Err(CompileError::MissingConstant {
      name: x.pretty(),
      caller: caller.into(),
    }),
    (_, None) => Err(CompileError::MissingConstant {
      name: y.pretty(),
      caller: caller.into(),
    }),
  }
}

/// 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).
pub fn compare_expr(
  x: &LeanExpr,
  y: &LeanExpr,
  mut_ctx: &MutCtx,
  x_lvls: &[Name],
  y_lvls: &[Name],
  stt: &CompileState,
) -> Result<SOrd, CompileError> {
  match (x.as_data(), y.as_data()) {
    (ExprData::Mvar(..), _) | (_, ExprData::Mvar(..)) => {
      Err(CompileError::UnsupportedExpr {