Function env_with_id

crates/kernel/src/def_eq.rs:1776–1796

()

    b: &KExpr<M>,
  ) {
    let Some(filter) = IX_PROJ_DELTA_TRACE.as_ref() else {
      return;
    };
    if !self.debug_label_matches_env() {
      return;
    }
    let id_s = id.to_string();
    if !filter.is_empty() && !id_s.contains(filter) {
      return;
    }
    log::info!(
      "[proj-delta] const={} depth={} phase={} proj={}.{} a={} b={}",
      self.debug_label.as_deref().unwrap_or("<unknown>"),
      self.def_eq_depth,
      phase,
      id,
      field,
      compact_def_eq_expr(a),
      compact_def_eq_expr(b)
    );
  }

  /// If the head of `e` is a projection, try reducing it via whnf_no_delta.
  /// Returns the reduced form if it changed, None otherwise (lean4lean tryUnfoldProjApp).