Function compare_kconst

crates/kernel/src/canonical_check.rs:458–537

Compare two block-eligible `KConst`s with full structural ordering. Different kinds order by `kconst_kind_ord`; same-kind dispatch goes to the kind-specific comparator. `resolve_ctor` is invoked for each Indc-vs-Indc comparison to fetch the concrete `KConst::Ctor` referenced by a ctor `KId`. The kernel caller threads a closure that consults `KEnv::get`.

(
  x: &KConst<M>,
  y: &KConst<M>,
  ctx: &KMutCtx,
  resolve_ctor: &dyn Fn(&KId<M>) -> Option<KConst<M>>,
)

  x: &KConst<M>,
  y: &KConst<M>,
  ctx: &KMutCtx,
  resolve_ctor: &dyn Fn(&KId<M>) -> Option<KConst<M>>,
) -> Result<SOrd, TcError<M>> {
  match (x, y) {
    (
      KConst::Defn { kind: xk, lvls: xl, ty: xt, val: xv, .. },
      KConst::Defn { kind: yk, lvls: yl, ty: yt, val: yv, .. },
    ) => compare_kdefn::<M>(*xk, *xl, xt, xv, *yk, *yl, yt, yv, ctx),
    (
      KConst::Indc {
        lvls: xl,
        params: xp,
        indices: xi,
        is_unsafe: xu,
        ty: xt,
        ctors: xc,
        ..
      },
      KConst::Indc {
        lvls: yl,
        params: yp,
        indices: yi,
        is_unsafe: yu,
        ty: yt,
        ctors: yc,
        ..
      },
    ) => compare_kindc::<M>(
      *xl,
      *xp,
      *xi,
      *xu,
      xt,
      xc,
      *yl,
      *yp,
      *yi,
      *yu,
      yt,
      yc,
      ctx,
      resolve_ctor,
    ),
    (
      KConst::Recr {
        lvls: xl,
        params: xp,
        indices: xi,
        motives: xm,
        minors: xn,
        k: xk,
        ty: xt,
        rules: xr,
        ..
      },
      KConst::Recr {
        lvls: yl,
        params: yp,