Expected Type in match

Stream: general

[Nima]

Is there anyway to explicitly tell lean the expected type of match, so I would not receive the following error:

invalid match/convoy expression, user did not provide type for the expression,
lean tried to infer one using expected type information, but result is not type correct

[Kenny Lau]

for example?

[Mario Carneiro]

match a, b : \forall a b, expected_type_of_match with ... end

[Mario Carneiro]

You can also often use type ascription in some cases, i.e. (match a, b with ... end : expected type)

[Nima]

OK, I don't have a good example for this.
Will get back if I found one.

[Nima]

Thank you, this following worked (the other one did not),

match a, b : \forall a b, expected_type_of_match with ... end