mcases generates expressions of the form \case a_1 \as x_1, ... a_n \as x_n \return T \with { ... }. We can allow additional arguments for \case, i.e., generate expressions of the form \case a_1 \as x_1, ... a_n \as x_n, b_1 : B_1, ... b_k : B_k \return T \with { ... }. These expressions won't be matched in the \case and are needed only because their type will changes in each clause.
I'm not sure about syntax yet. Also, we can have a separate syntax for the special case when b_i : B_i is idp : a_j = x_j.
mcasesgenerates expressions of the form\case a_1 \as x_1, ... a_n \as x_n \return T \with { ... }. We can allow additional arguments for \case, i.e., generate expressions of the form\case a_1 \as x_1, ... a_n \as x_n, b_1 : B_1, ... b_k : B_k \return T \with { ... }. These expressions won't be matched in the \case and are needed only because their type will changes in each clause.I'm not sure about syntax yet. Also, we can have a separate syntax for the special case when
b_i : B_iisidp : a_j = x_j.