Method wrap_with_block_param_foralls

crates/kernel/src/inductive.rs:991–1016

Wrap `body` with `∀ T_0 T_1 ... T_{n-1}, body` using the supplied block-param binders (outermost-first). Mirrors compile-side `mk_forall(body, &block_param_decls)`. # de Bruijn convention Inside `body`, free `Var(i)` for `i < n_block_params` refers to block param at position `n_block_params - 1 - i` in the recursor-external context (because spec_params follow this pattern). After the wrap, `Var(n

(
    &mut self,
    body: KExpr<M>,
    binders: &[(
      M::MField<ix_common::env::Name>,
      M::MField<ix_common::env::BinderInfo>,
      KExpr<M>,
    )],
  )

    })();
    self.lctx.truncate(saved_lctx);
    result
  }

  /// Rewrite nested occurrences in synthetic aux member/ctor types to the
  /// corresponding synthetic aux constants before running `sort_consts`
  /// partition refinement. Compile-side `expand_nested_block` does this via
  /// its queue pass over all expanded constructors; the kernel has already
  /// discovered the flat aux set, so it can rewrite by matching each
  /// occurrence against that set.
  fn replace_aux_refs_for_sort(
    &mut self,
    e: &KExpr<M>,
    aux: &[FlatBlockMember<M>],
    aux_ids: &[KId<M>],
    block_us: &[KUniv<M>],
    n_block_params: u64,
    local_depth: u64,
  ) -> Result<KExpr<M>, TcError<M>> {
    if let Some(replaced) = self.try_replace_aux_ref_for_sort(
      e,
      aux,
      aux_ids,
      block_us,
      n_block_params,
      local_depth,
    )? {
      return Ok(replaced);
    }