Open isovector opened 3 years ago
https://github.com/isovector/haskell-language-server/blob/8e690047025ec05e92c69a3536cba9669f3e18e2/plugins/tactics/src/Ide/Plugin/Tactic.hs#L335-L346 implements this for function RHSes. The more general solution is likely to just extend this.
That is, if i write
the hole should get
(foo.[[a,b,c]])
inserted in its position vars judgement