Method try_def_eq_app

crates/kernel/src/def_eq.rs:1258–1282

App spine comparison (lean4lean isDefEqApp): decompose both sides into head + args and compare componentwise. Handles multi-arg apps.

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

    // Inductive must be struct-like (non-recursive, 0 indices, 1 ctor)
    if !self.is_struct_like(&induct_id)? {
      self.dump_eta_trace("not-struct-like", Some(&induct_id), 0, &t_norm, s);
      return Ok(false);
    }

    // Types must be def-eq (lean4lean tryEtaStructCore, line 515).
    // 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)) {
      Ok(ty) => ty,
      Err(_) => {
        self.dump_eta_trace("infer-lhs-type", Some(&induct_id), 0, &t_norm, s);
        return Ok(false);
      },
    };
    if !self.is_def_eq(&t_ty, &s_ty)? {
      self.dump_eta_trace("type-mismatch", Some(&induct_id), 0, &t_norm, s);
      return Ok(false);
    }