You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
Remove => {?}
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:
Replace => {?} with \elim <caret>, which should be a template.
After you fill in the parameters and finish the template, IDE should generate clauses.
The text was updated successfully, but these errors were encountered:
marat-rkh
changed the title
Intention to generate pattern patching clauses
Intention to generate pattern matching clauses
May 7, 2021
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:=> {?}
\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:=> {?}
with\elim <caret>
, which should be a template.The text was updated successfully, but these errors were encountered: