Function mut_const_kind

crates/compile/src/compile.rs:2796–2802

Returns a kind ordinal for cross-kind comparison of mutual constants.

(c: &MutConst)

  match (x.as_data(), y.as_data()) {
    (LevelData::Mvar(..), _) | (_, LevelData::Mvar(..)) => {
      Err(CompileError::UnsupportedExpr {
        desc: "level metavariable in comparison".into(),
      })
    },
    (LevelData::Zero(_), LevelData::Zero(_)) => Ok(SOrd::eq(true)),
    (LevelData::Zero(_), _) => Ok(SOrd::lt(true)),
    (_, LevelData::Zero(_)) => Ok(SOrd::gt(true)),
    (LevelData::Succ(x, _), LevelData::Succ(y, _)) => {
      compare_level(x, y, x_ctx, y_ctx)
    },