CodingCellist
CodingCellist
I was playing around with sirdi for an existing project today, and noticed that my `.ipkg` file (which I was using for interactive editing purposes) was gone. I managed to...
- [x] I have read [CONTRIBUTING.md](https://github.com/idris-lang/Idris2/blob/main/CONTRIBUTING.md). - [x] I have checked that there is no existing PR/issue about my proposal. ## Summary Prompted by a question from locria/locriacyber and spotted...
# Steps to Reproduce Consider the following code which uses @-patterns, `case`, and auto-implicits: ```idris module CaseLetAuto import Data.Maybe foo : (t : Maybe Nat) -> {auto 0 tOK :...
**Does this bug happen when you install plugin without vim-polyglot?** No **Describe the bug:** When writing an Idris2 file with existing `shiftwidth` defined, its value gets set to 8 on...
The default keybindings have been mentioned to conflict with Ubuntu (#159). I believe my issue is more general, as it seems the default keybindings conflict with the "Terminator" terminal emulator...
How to reproduce: 1. Open a `.idr` file in Atom, it should contain an executable function, e.g. (from the book): ``` module Main import System countdown : (secs : Nat)...
How to reproduce: 1. Crash the Idris plugin like in #223 2. Close the crashed REPL and attempt to open a new one through `Ctrl`+`Alt`+`Enter`. **Atom**: 1.33.1 x64 **Electron**: 3.0.13...
When trying to install Idris using `stack`, the following error-messages appear: ``` Error: While constructing the build plan, the following exceptions were encountered: In the dependencies for idris-1.3.1: Cabal-2.4.1.0 from...
Cycle detection when resolving metavariables is considered valid `impossible` cases (see `src/TTImp/ProcessDef.idr:142`), so they should probably also be considered unrecoverable errors since, afaiu, "recoverable" errors are ones where you could...
# Steps to Reproduce Case-split on `cmd` in the following code: ```idris data ISM : Type -> Nat -> Nat -> Type where CMD_INIT : (n : Nat) -> ISM...