Function compare_const

crates/compile/src/compile.rs:2807–2834

Compare two mutual constants with caching. Dispatches to the appropriate type-specific comparator (defn, indc, recr). Different-kind constants are ordered by kind tag.

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

    },
    (LevelData::Succ(_, _), _) => Ok(SOrd::lt(true)),
    (_, LevelData::Succ(_, _)) => Ok(SOrd::gt(true)),
    (LevelData::Max(xl, xr, _), LevelData::Max(yl, yr, _)) => {
      SOrd::try_compare(compare_level(xl, yl, x_ctx, y_ctx)?, || {
        compare_level(xr, yr, x_ctx, y_ctx)
      })
    },
    (LevelData::Max(_, _, _), _) => Ok(SOrd::lt(true)),
    (_, LevelData::Max(_, _, _)) => Ok(SOrd::gt(true)),
    (LevelData::Imax(xl, xr, _), LevelData::Imax(yl, yr, _)) => {
      SOrd::try_compare(compare_level(xl, yl, x_ctx, y_ctx)?, || {
        compare_level(xr, yr, x_ctx, y_ctx)
      })
    },
    (LevelData::Imax(_, _, _), _) => Ok(SOrd::lt(true)),
    (_, LevelData::Imax(_, _, _)) => Ok(SOrd::gt(true)),
    (LevelData::Param(x, _), LevelData::Param(y, _)) => {
      match (
        x_ctx.iter().position(|n| x == n),
        y_ctx.iter().position(|n| y == n),
      ) {
        (Some(xi), Some(yi)) => Ok(SOrd::cmp(&xi, &yi)),
        (None, _) => Err(CompileError::UnknownUnivParam {
          curr: String::new(),
          param: x.pretty(),
        }),
        (_, None) => Err(CompileError::UnknownUnivParam {
          curr: String::new(),
          param: y.pretty(),
        }),
      }
    },