Function def_eq_const_diff_addr

crates/kernel/src/def_eq.rs:1909–1915

()

/// Extract head constant KId from expression or app spine.
fn head_const_id<M: KernelMode>(e: &KExpr<M>) -> Option<KId<M>> {
  match e.data() {
    ExprData::Const(id, _, _) => Some(id.clone()),
    ExprData::App(..) => {
      let head = app_head(e);
      match head.data() {
        ExprData::Const(id, _, _) => Some(id.clone()),
        _ => None,
      }
    },
    _ => None,