Function mk_lambda

crates/compile/src/compile/aux_gen/expr_utils.rs:447–449

Build a lambda chain by batch-abstracting all FVars in a single pass. Same semantics as `mk_forall` but produces `λ (x : T), body`.

(body: LeanExpr, binders: &[LocalDecl])

///
/// Same semantics as `mk_forall` but produces `λ (x : T), body`.
pub fn mk_lambda(body: LeanExpr, binders: &[LocalDecl]) -> LeanExpr {
  mk_binder_chain(body, binders, BinderKind::Lambda)
}

/// Whether to build forall or lambda binders.
#[derive(Clone, Copy)]