voile::check::expr
fn check_app_type(tcs: TCS, f: &Abs, info: Loc, a: &Abs, pi_ty: &Val) -> ValTCM
Recursive function to insert meta for implicit argument