Pattern match with hint on types

Stream: lean4

[Z. Wu]

Hi, I'm wondering if there's a simple syntax for providing type and motive for a match. Here's an example of what I want to achieve. In the following code, I want to tell lean that a is of type TypeA and use motive as the motive function when calling casesOn:

match (a: TypeA) returning motive with
| .Case1 _ _ x => x

I know I can probably go let x: TypeA := a; @TypeA.casesOn ... (motive:=motive) x ... but it would be nice if I can stick with match.

[Marcus Rossel]

example := fun a =>
  show Int from match (a : Nat × Nat) with
  | .mk _ _ => 10

[Arthur Adjedj]

You can use motive to do that:

#check fun n : Nat =>
  match (motive := (n : Nat) -> Fin (n+1)) n with
    | 0 => ⟨0,Nat.lt_succ_self 0⟩
    | n+1 => ⟨n+1,Nat.lt_succ_self (n+1)⟩

[Z. Wu]

Thanks!