Function def_eq_const_same

crates/kernel/src/def_eq.rs:1881–1887

()

fn compact_def_eq_head<M: KernelMode>(e: &KExpr<M>) -> String {
  let (head, args) = collect_app_spine(e);
  let base = match head.data() {
    ExprData::Var(i, _, _) => format!("#{i}"),
    ExprData::FVar(id, _, _) => format!("{id}"),
    ExprData::Sort(u, _) => format!("Sort({u})"),
    ExprData::Const(id, us, _) => format!("{id}.{{{}}}", us.len()),
    ExprData::App(..) => "app".to_string(),
    ExprData::Lam(..) => "lam".to_string(),
    ExprData::All(..) => "forall".to_string(),
    ExprData::Let(..) => "let".to_string(),