intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

Make "Fill goal" available before closing curly bracket

Open marat-rkh opened this issue 3 years ago • 0 comments

Screen Shot 2021-10-27 at 3 06 00 PM

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>}.

marat-rkh avatar Oct 27 '21 12:10 marat-rkh