Method quick_def_eq

crates/kernel/src/def_eq.rs:557–603

Quick structural: same constructor, recursively same children (no WHNF).

(
    &mut self,
    a: &KExpr<M>,
    b: &KExpr<M>,
  )

    if wa_changed || wb_changed {
      return self.is_def_eq(&wa_core, &wb_core);
    }
    let wa = wa_core;
    let wb = wb_core;
    if wa.ptr_eq(&wb) {
      return Ok(true);
    }
    if self.quick_def_eq(&wa, &wb)? {
      return Ok(true);
    }

    // Tier 4d: app spine comparison (lean4lean isDefEqApp, lean4 type_checker.cpp:1115)
    if self.try_def_eq_app(&wa, &wb)? {
      return Ok(true);
    }

    let result = self.is_def_eq_whnf(&wa, &wb);

    // Tier 5 final-fail trace: when IX_DEF_EQ_TIER5_DUMP is set and the
    // pair's head names contain the configured substring, dump the
    // post-whnfCore wa/wb. This is where lazy-delta + Tier 4c gave up.
    if let Ok(prefix) = crate::env_var("IX_DEF_EQ_TIER5_DUMP")
      && let Ok(false) = result.as_ref()
    {
      let a_match = head_const_name(&wa).is_some_and(|n| n.contains(&prefix));
      let b_match = head_const_name(&wb).is_some_and(|n| n.contains(&prefix));
      if prefix.is_empty() || a_match || b_match {
        log::info!("[deq tier5 fail] depth={}", self.def_eq_depth);
        log::info!("  wa: {wa}");
        log::info!("  wb: {wb}");
      }
    }

    result
  }

  /// Quick structural: same constructor, recursively same children (no WHNF).
  fn quick_def_eq(
    &mut self,
    a: &KExpr<M>,
    b: &KExpr<M>,
  ) -> Result<bool, TcError<M>> {
    match (a.data(), b.data()) {
      (ExprData::Sort(u1, _), ExprData::Sort(u2, _)) => Ok(univ_eq(u1, u2)),
      (
        ExprData::Lam(name, bi, ty1, body1, _),
        ExprData::Lam(_, _, ty2, body2, _),
      )
      | (
        ExprData::All(name, bi, ty1, body1, _),
        ExprData::All(_, _, ty2, body2, _),