idris-lang
Add --use-ipkg flag, and more refactoring
Please refrain from needlessly reflowing code by moving = do to a prior line. It makes seeing the actual changes harder
Sorry, should I submit a new patch? My editor gets confused by oddly indented code (indent/reindent only stop at tab break).
Sorry, should I submit a new patch?
No need. You can update a PR by pushing to the same branch.
The indentation in preOption has also been modified in such a way that it would not be stable under
alpha-renaming. Please stick to the original style across the files (cf. https://github.com/edwinb/Yaffle/blob/main/CONVENTIONS.md#conventions for a brief description of the essentials).
Sorry, but I'm not sure where I need to modify.
Is there a plan to indent current codebase consistently first?
As for the diff, VS Code automatically remove indent changes in diff of Idris files (and other languages as well). Maybe it will help you view diff better? Maybe there are CLI tools that do it too.
I'm not intending to install new tools to compensate for needless reflowing. Just do not introduce the needless reflowing in the first place.
Looks like this has stalled because of styling changes.
@locriacyber there is currently no style guide for Idris 2 and no plan to enforce one. Idris2 is still a young language with very few people using it so there is no established way to write it "correctly" (when should you use ! and when should you use <$>?) and nobody has enough time to bikeshed and enforce a style guide. For now, the rule is to leave the code better than you found it, but reflowing the code does not achieve that in this specific instance.
@locriacyber If I understand correctly @gallais 's intent you should write
preOption NoBanner
= tuneSession { nobanner := True }
is that right @gallais ?
My own feedback is that there is no need for ControlFlow to be in its own module and to take two type arguments since they are only ever used in SetOptions and only ever used with Unit
I'm going to close this given it's gone stale and we haven't heard from OP in a year