Case split using <LocalLeader>c does not work

[apriori]

Test case (written manually, due to #10):

Case split on xs:

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs

Idris internal error: Internal error: "xs is not a pattern variable"

Versions:

idris 0.9.12 (cabal) idris-vim 25866452141e2ab9ecc642a9682f4a9a76501063 (current HEAD)

[edwinb]

This isn't anything to do with vim mode, but rather idris itself. Interactive editing requires there to be an idris instance running, with the file being edited being in its working directory. This error would come up if the file was in a different directory.

If you do ':cs xs ' at the Idris prompt with your file open, do you get the right case split as output?

If it's not that, please can you say everything about what you did? (And I mean everything in the sense that I need to know what files are open, where the Idris instance is, etc.)

Edwin.

On 12 Apr 2014, at 13:48, apriori notifications@github.com wrote:

Test case (written manually, due to #10):

Case split on xs:

append : Vect n a -> Vect m a -> Vect (n + m) a append xs ys = ?append_rhs Idris internal error: Internal error: "xs is not a pattern variable"

Versions:

idris 0.9.12 (cabal) idris-vim 2586645 (current HEAD)

— Reply to this email directly or view it on GitHub.

[apriori]

Well, interesting. If I open the file using idris repl (idris test.idr) everything, including creation of the template (see #10) works just fine. But if I use the more explicit form "idris ./test.idr", template creation and case split fails.