pub fn elaborate(
ctx: &Context,
mctx: &mut MetaCtx,
term: &Term,
expected: Option<&Term>,
) -> KernelResult<(Term, Term)>Expand description
Elaborate term (which may contain Holes) against an optional expected type,
solving the holes by unification. Returns the elaborated term and its type (both still
containing metavariables until instantiated).