We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The indentation of clauses added by <LocalLeader>m depends on the position of the cursor at the time of invocation. Given the following example,
<LocalLeader>m
data Foo = Bar | Baz | Quux foo : Foo -> Foo foo Bar = ?foo_rhs
placing the cursor on the 'B' of the Bar pattern, followed by invoking <LocalLeader>m results in this
Bar
foo : Foo -> Foo foo Bar = ?foo_rhs foo Quux = ?Bar_rhs_1 foo Baz = ?Bar_rhs_2
Invoking the command at the beginning of the line works as expected, placing the latter two equations in the first column.
The text was updated successfully, but these errors were encountered:
It was fixed upstream in idris-lang/Idris-dev#3869 (but will of course take some time to become part of a release), so this can be closed.
Sorry, something went wrong.
No branches or pull requests
The indentation of clauses added by
<LocalLeader>m
depends on the position of the cursor at the time of invocation. Given the following example,placing the cursor on the 'B' of the
Bar
pattern, followed by invoking<LocalLeader>m
results in thisInvoking the command at the beginning of the line works as expected, placing the latter two equations in the first column.
The text was updated successfully, but these errors were encountered: