Method is_regular

crates/kernel/src/def_eq.rs:1305–1311

Check if a constant has Regular reducibility hints (not Abbrev or Opaque). Used to guard the same-head-spine optimization (lean4lean: dt.hints.isRegular).

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

    // No Prop guard here — struct eta in def-eq is safe even for Prop types
    // because we're checking equality, not constructing terms. The Prop guard
    // is only needed in iota's toCtorWhenStruct (whnf.rs try_struct_eta_iota)
    // where eta-expanding creates projections that would be unsound for Prop.
    let s_ty = match self.with_infer_only(|tc| tc.infer(s)) {
      Ok(ty) => ty,
      Err(_) => {
        self.dump_eta_trace("infer-rhs-type", Some(&induct_id), 0, t, s);
        return Ok(false);
      },
    };
    let t_ty = match self.with_infer_only(|tc| tc.infer(&t_norm)) {