Function compile_const_inner

crates/compile/src/compile.rs:3189–3460

(
  name: &Name,
  all: &NameSet,
  lean_env: &Arc<LeanEnv>,
  cache: &mut BlockCache,
  stt: &CompileState,
  kctx: &mut KernelCtx,
  aux: bool,
)

                  },
                )
              })
            })
          })
        })
      })
    },
  )
}

/// Returns a kind ordinal for cross-kind comparison of mutual constants.
fn mut_const_kind(c: &MutConst) -> u8 {
  match c {
    MutConst::Defn(_) => 0,
    MutConst::Indc(_) => 1,
    MutConst::Recr(_) => 2,
  }
}

/// Compare two mutual constants with caching. Dispatches to the appropriate
/// type-specific comparator (defn, indc, recr). Different-kind constants
/// are ordered by kind tag.
pub fn compare_const(
  x: &MutConst,
  y: &MutConst,
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
) -> Result<Ordering, CompileError> {
  let (key, reversed) = if x.name() <= y.name() {
    ((x.name(), y.name()), false)
  } else {
    ((y.name(), x.name()), true)
  };
  if let Some(so) = cache.cmps.get(&key) {
    return Ok(if reversed { so.reverse() } else { *so });
  }
  let so: SOrd = match (x, y) {
    (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> {