Function compile_clauses 

pub fn compile_clauses(
    ctx: &Context,
    scrutinees: &[Term],
    result_type: &Term,
    clauses: &[Clause],
) -> KernelResult<Term>

Compile a clause matrix against a list of scrutinees.

result_type is the match’s motive at every node: a raw type, which the kernel wraps as the constant motive λ_:I. result_type.

Returns the compiled term. Use compile_clauses_reporting when the caller wants the unreachable-clause census as well.