Method eta_expansion_base

crates/kernel/src/def_eq.rs:1229–1254

(
    &mut self,
    induct_id: &KId<M>,
    num_params: usize,
    num_fields: usize,
    args: &[KExpr<M>],
  )

    let ctor_id = match s_head.data() {
      ExprData::Const(id, _, _) => id.clone(),
      _ => {
        self.dump_eta_trace("rhs-not-ctor-head", None, 0, &t_norm, s);
        return Ok(false);
      },
    };

    // Head must be a constructor
    let (induct_id, num_params, num_fields) = match self
      .try_get_const(&ctor_id)?
    {
      Some(KConst::Ctor { induct, params, fields, .. }) => {
        (induct.clone(), u64_to_usize::<M>(params)?, u64_to_usize::<M>(fields)?)
      },
      _ => {
        self.dump_eta_trace("rhs-head-not-ctor", Some(&ctor_id), 0, &t_norm, s);
        return Ok(false);
      },
    };

    // Must be fully applied
    if s_args.len() != num_params + num_fields {
      self.dump_eta_trace(
        "ctor-arity",
        Some(&ctor_id),
        s_args.len(),
        &t_norm,
        s,
      );
      return Ok(false);