Method mk_lambda

crates/kernel/src/lctx.rs:139–147

Abstract `body` over `fvars` and wrap it in a chain of `Lam` (or `Let` for `LDecl` entries) binders, innermost-first. The result has all of the listed fvars replaced by de Bruijn indices (`fvars[0]` becomes the outermost binder, `fvars[n-1]` the innermost). This is the inverse of the binder-opening pattern used during type checking: open with [`NameGenerator::fresh`], recurse, close back here so

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

  ///
  /// Mirrors `Lean.LocalContext.mkLambda`.
  pub fn mk_lambda(
    &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 */ true)
  }

  /// Abstract `body` over `fvars` and wrap it in a chain of `All` (or `Let`
  /// for `LDecl` entries) binders, innermost-first.