Method is_struct_like

crates/kernel/src/whnf.rs:1041–1048

(&mut self, id: &KId<M>)

  /// because Ix relies on the no-delta layer for primitive/native reductions,
  /// but it preserves Lean's cheap projection policy for projected values.
  pub(super) fn whnf_no_delta_for_def_eq(
    &mut self,
    e: &KExpr<M>,
  ) -> Result<KExpr<M>, TcError<M>> {
    self.cheap_recursion_depth += 1;
    let result =
      self.whnf_no_delta_impl(e, WhnfFlags::DEF_EQ_CORE, NatSuccMode::Collapse);
    self.cheap_recursion_depth -= 1;
    result
  }