Method try_string_lit_expansion

crates/kernel/src/def_eq.rs:1003–1014

String literal expansion (C++ kernel: try_string_lit_expansion_core). When `t` is a string literal, expand it to constructor form via `str_lit_to_constructor` (String.ofList [Char.ofNat c₁, ...]), WHNF the result so String.ofList + Char.ofNat delta-unfold to the canonical `String.ofByteArray ...` form, then compare with `s`.

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

  /// Def-eq for nat-like values: handles mixed literal/constructor comparison.
  /// Fast-path: two Nat literals are compared directly by value (O(1) instead of
  /// O(n) recursion depth that would blow the def_eq_depth limit).
  fn is_def_eq_nat(
    &mut self,
    a: &KExpr<M>,
    b: &KExpr<M>,
  ) -> Result<bool, TcError<M>> {
    // Fast path: both literals — compare by value directly
    if let (ExprData::Nat(va, _, _), ExprData::Nat(vb, _, _)) =
      (a.data(), b.data())
    {
      return Ok(va == vb);
    }
    if self.is_nat_zero(a) && self.is_nat_zero(b) {
      return Ok(true);
    }