Method insert_implicits

leanr-elab/src/implicit.rs:22–34

Insert implicit arguments for a function application

(
        &mut self,
        func_type: TermId,
        arena: &Arena,
        depth: u32,
    )

    /// Insert implicit arguments for a function application
    pub fn insert_implicits(
        &mut self,
        func_type: TermId,
        arena: &Arena,
        depth: u32,
    ) -> ElabResult<Vec<TermId>> {
        let mut implicits = Vec::new();

        // TODO: Walk through Pi type and insert metavariables for implicit params
        // For now, return empty vec

        Ok(implicits)
    }

    /// Get the metavariable context
    pub fn mctx(&self) -> &MetaVarContext {