Method build_lambda

leanr-elab/src/elaborate.rs:536–554

Build lambda from params

(&mut self, params: Vec<Param>, body: TermId)

    /// Build lambda from params
    fn build_lambda(&mut self, params: Vec<Param>, body: TermId) -> ElabResult<TermId> {
        let mut result = body;

        for param in params.into_iter().rev() {
            let ty = if let Some(ref ty_expr) = param.type_ {
                self.synth(ty_expr)?.0
            } else {
                self.fresh_mvar()?
            };

            for name in param.names.into_iter().rev() {
                let name_sym = self.arena.get_symbol(&name.name);
                let binder = Binder::new(name_sym, ty);
                result = self.arena.mk_lam(binder, result);
            }
        }

        Ok(result)
    }

    /// Create a fresh metavariable
    fn fresh_mvar(&mut self) -> ElabResult<TermId> {