intellij-arend
intellij-arend copied to clipboard
Make "Fill goal" available before closing curly bracket

In this example, the caret is placed like this: {?(foldr-monoid<caret>)}
. As you can see, there is no "Fill goal" in the context menu. To invoke it, I need to place the caret at the ?
symbol. Jumping back like that is inconvenient. It would be much better to make "Fill goal" available at {?(foldr-monoid<caret>)}
or at {?(foldr-monoid)<caret>}
.