Method mk_pi

crates/kernel/src/lctx.rs:154–162

Abstract `body` over `fvars` and wrap it in a chain of `All` (or `Let` for `LDecl` entries) binders, innermost-first. Same shape as [`Self::mk_lambda`] but emits `All` for `CDecl` entries. Mirrors `Lean.LocalContext.mkForall`.

(
    &self,
    intern: &mut InternTable<M>,
    fvars: &[FVarId],
    body: &KExpr<M>,
  )

  /// Same shape as [`Self::mk_lambda`] but emits `All` for `CDecl` entries.
  /// Mirrors `Lean.LocalContext.mkForall`.
  pub fn mk_pi(
    &self,
    intern: &mut InternTable<M>,
    fvars: &[FVarId],
    body: &KExpr<M>,
  ) -> KExpr<M> {
    let abstracted = abstract_fvars(intern, body, fvars);
    self.wrap_binders(intern, fvars, abstracted, /* as_lambda */ false)
  }

  fn wrap_binders(
    &self,