Intention to generate pattern matching clauses

[marat-rkh]

Suppose I have some function: \func foo (n m : Nat) : Bool => {?}

Naturally, I first write its signature and leave => {?} as a result, because I don't know what will be there. Now I realize I want to do a pattern matching. Currently, I can do it like this:

1. Remove => {?}
2. Jump to error at \func that says "Some clauses are missing" and invoke a quick fix to generate them.

I think having an intention to do these 2 steps in one go would be more convenient. That intention should be available at {?}. A similar intention for pattern matching with \elim could be added too. It would:

1. Replace => {?} with \elim <caret>, which should be a template.
2. After you fill in the parameters and finish the template, IDE should generate clauses.