Skip to content

Conversation

@WizardOfMenlo
Copy link

Apparently, the ordering of the command arguments was giving issue to some users (me included) as detailed in #19 .
Not sure why this is needed, as the help for idris2 seems to suggest to have [options] [input file], but apparently this is the case.

@WizardOfMenlo WizardOfMenlo changed the title Fix #19 Fix positional error mentioned in #19 Dec 3, 2020
@BorisNikulin
Copy link

BorisNikulin commented Dec 4, 2020

This sort of fixes it? I applied the patch manually and observed the plugin working more than before but not as I thought it would work with in place editing, such as writing in the cases on case split.

When using the plugin most commands had no output or in place edits. However, when manually pulling up the response window with \i some commands produced output. Namely \c and \mc with the same output of

Strangely \d for docs , \t for type of, and \p for proof search also returns that.

After putting the function case equation back and thus satisfying the type checker, there is no output in the response window at all from the commands tried above.

\r for loading the file into the REPL (via vim terminal? or idris2 IDE mode?) still has the file not found problem.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants