Method str_lit_to_constructor

crates/kernel/src/def_eq.rs:1021–1056

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.

(&mut self, s: &str)

      (Some(a_pred), Some(b_pred)) => self.is_def_eq(&a_pred, &b_pred),
      _ => Ok(false),
    }
  }

  /// M2: Nat offset reduction for lazy delta loop (lean4lean isDefEqOffset),
  /// generalized to offset form: each side decomposes to `base + offset`
  /// (`Lit n`, `succ` layers, and `Nat.add base (Lit m)` — the compact stuck
  /// form WHNF now leaves — all read in O(1) per layer), the shared offset
  /// is stripped in ONE step, and the remainders compare through full
  /// def-eq. This collapses `succ^k(x) ≟ succ^k(x)` from k `is_def_eq`
  /// recursion levels (which blew `MAX_DEF_EQ_DEPTH` for large k) to one.
  /// Stripping is verdict-preserving: `+k` is definitionally injective, the
  /// same semantics the previous one-succ-peel already relied on.
  /// Non-offset shapes fall back (`None`) to the generic path unchanged.
  fn try_def_eq_offset(
    &mut self,
    a: &KExpr<M>,
    b: &KExpr<M>,
  ) -> Result<Option<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(Some(va == vb));
    }
    if self.is_nat_zero(a) && self.is_nat_zero(b) {
      return Ok(Some(true));
    }
    // Allocation-free quick reject: decompose walks app spines, so only run
    // it when both heads are plausibly offset-shaped (the old one-succ-peel
    // rejected non-Nat shapes in O(1) off `e.data()` — keep that property).
    if !self.nat_offset_candidate(a) || !self.nat_offset_candidate(b) {
      return Ok(None);
    }
    let Some((base_a, ka)) = self.nat_offset_decompose(a)? else {
      return Ok(None);
    };
    let Some((base_b, kb)) = self.nat_offset_decompose(b)? else {
      return Ok(None);
    };