Function fill_match_motives 

pub fn fill_match_motives(
    ctx: &Context,
    term: &Term,
    expected: Option<&Term>,
) -> KernelResult<Term>

Fill in inferred motives for match expressions written WITHOUT a return clause (the Hole motive the parser leaves). The motive is a CONSTANT λ_:I. T — covering non-dependent matches — where T is the EXPECTED type (a definition’s declared result type, propagated through binders) or, lacking one, the type of a nullary first branch. The pass threads the kernel context through binders so the discriminant’s type resolves; a match it cannot give a motive (a dependent case, no expected type) is reported so the user can add an explicit return.