Function def_eq_all_structural

crates/kernel/src/def_eq.rs:1927–1933

()

/// Meta mode. Returns `None` if the head isn't a `Const`.
fn head_const_name<M: KernelMode>(e: &KExpr<M>) -> Option<String> {
  let id = head_const_id(e)?;
  Some(format!("{id}"))
}

impl<M: KernelMode> TypeChecker<'_, M> {
  fn dump_def_eq_max(
    &self,
    kind: &str,
    a: &KExpr<M>,
    b: &KExpr<M>,