Method try_eta_struct

crates/kernel/src/def_eq.rs:1101–1227

Struct eta (lean4lean style): if `s` is a fully-applied constructor of a struct-like type, check `proj(i, t) ≡ s.args[params+i]` for each field. Tries `tryEtaStructCore(t, s)` — caller should try both directions.

(
    &mut self,
    t: &KExpr<M>,
    s: &KExpr<M>,
  )

      return Ok(*s_val == str_val);
    }
    let expanded = self.str_lit_to_ctor_app(&str_val)?;
    self.is_def_eq(&expanded, s)
  }

  /// Convert a string literal to constructor form:
  /// `"abc"` → `String.ofList (List.cons (Char.ofNat 97) (List.cons (Char.ofNat 98) (... List.nil)))`
  ///
  /// Uses `Char.ofNat` (not `Char.mk`) matching lean4lean/C++ kernel.
  /// Uses `String.ofList` (= `String.mk` in our env) matching lean4lean/C++ kernel.
  pub(super) fn str_lit_to_constructor(&mut self, s: &str) -> KExpr<M> {
    let char_const =
      self.intern(KExpr::cnst(self.prims.char_type.clone(), Box::new([])));
    let char_of_nat =
      self.intern(KExpr::cnst(self.prims.char_of_nat.clone(), Box::new([])));
    let string_mk =
      self.intern(KExpr::cnst(self.prims.string_of_list.clone(), Box::new([])));

    // List.nil.{0} Char
    let list_nil_z = self.intern(KExpr::cnst(
      self.prims.list_nil.clone(),
      Box::new([KUniv::zero()]),
    ));
    let nil = self.intern(KExpr::app(list_nil_z, char_const.clone()));

    // List.cons.{0} Char
    let list_cons_z = self.intern(KExpr::cnst(
      self.prims.list_cons.clone(),
      Box::new([KUniv::zero()]),
    ));
    let cons = self.intern(KExpr::app(list_cons_z, char_const));

    // Build list right-to-left: foldr
    let mut list = nil;
    for c in s.chars().rev() {
      let nat_val = bignat::Nat::from(c as u64);
      let nat_addr = ix_common::address::Address::hash(&nat_val.to_le_bytes());
      let nat_lit = self.intern(KExpr::nat(nat_val, nat_addr));
      let char_val = self.intern(KExpr::app(char_of_nat.clone(), nat_lit));
      let partial = self.intern(KExpr::app(cons.clone(), char_val));
      list = self.intern(KExpr::app(partial, list));
    }

    // String.mk list
    self.intern(KExpr::app(string_mk, list))
  }

  /// String literal → structure-constructor application.
  ///
  /// `str_lit_to_constructor` produces `String.ofList [Char.ofNat c…]`;
  /// with the native collapse rule in `try_reduce_string`, a whnf of
  /// that application folds straight back into the `Str` literal. So
  /// callers that need the actual constructor form — iota majors,
  /// projections, literal-vs-structural def-eq — take one delta step
  /// past `String.ofList` here: in the compiled environment that
  /// exposes `String.ofByteArray (List.utf8Encode [chars]) proof`
  /// (fields stay lazy). In environments where the `String.ofList`
  /// address IS the constructor (List-Char-model test envs), the delta
  /// step is a no-op and the expansion is already ctor-headed.