Case-split on bind patterns

[imkiva]

No description provided.

[ice1000]

Did you mean case-splits on bind patterns?

[imkiva]

Did you mean case-splits on bind patterns?

Yes, but called inside a hole (like C-c C-c in agda mode)

[ice1000]

Did you mean case-splits on bind patterns?

Yes, but called inside a hole (like C-c C-c in Agda mode)

We don't need to enforce quick-fixes to be in holes. We can make them happen everywhere. I think Agda mode does this due to their poor IDE support

[imkiva]

Did you mean case-splits on bind patterns?

Yes, but called inside a hole (like C-c C-c in Agda mode)

We don't need to enforce quick-fixes to be in holes. We can make them happen everywhere. I think Agda mode does this due to their poor IDE support

Ohhh yes! It should be an action for all bind patterns. Like the "put parameters on separate lines" for Java