Steve Dunham
Steve Dunham
This PR addresses #2513 by adding a rig to ICase. It includes a test case named `idris2/linear016`. It needs to be double checked by someone familiar with elaboration of case...
Idris appears to be leaking memory in FFI on scheme. This was first noticed because the LSP process was growing as I was working on Idris. Repeatedly reloading a touched...
This change allows users to forward declare `record`, like they can for `data`, by omitting the `where` clause. The implementation follows the pattern of same functionality for `data`. After the...
Switch to the more modern go modules layout.
This feature isn't documented at all and is a common use case.
Not sure what, if anything can be done to deal with this, but I figured I'd note the issue. OSX Mojave is locking down the backup directory to the point...
Apple has dropped the extra encryption on iOS 10.2, so we can list files, etc, without the password again. Push the password prompt back to when the keys are first...
There is a mostly complete notes2md locally, finish it and check it in.
# Description Add documentation for the `%cg` pragma. I missed this one when documenting the pragmas because it is hiding in the lexer.
Idris appears to be accepting a program that matches on an erased value. # Steps to Reproduce Type check this code: ```idris data Foo : Type where NoFoo : Foo...