Steve Dunham
Steve Dunham
I'm seeing unification errors in multi-`with` statements that go away when they are split out into separate `with` statements. Below is a reduced test case ([also available in this gist](https://gist.github.com/dunhamsteve/cc8634a6005893aca2308e7de4758e79))....
This PR builds on the work of @gallais in #2 to get SPLV20 to build with the latest version of Idris2. It also changes the code to use the new...
idris-community/idris2-lsp#197 adds a new configuration option to control the behavior of text completions in the LSP. It allows users to choose to have tab completion with just the function name...
This PR injects the `source.idris` into `idris` markdown code blocks in visual studio code. This will give us the base textmate highlighting and support for the comment commands within those...
# Description The PR enhances totality checking to see size changes underneath matching constructors, addressing issue #3317. With this change Idris recognizes: - `Just xs` is smaller than `Just (x...
# Description This PR addresses a few issues in #2250 and issue #3276. They are caused by an issue with `IAlternative` in impossible clauses, a type confusion issue in impossible...
This is another attempt at PR #3328, which addresses #3317. PR #3328 was merged but later reverted because of a performance regression in some cases (#3354 - the compiler hangs)....
# Steps to Reproduce The compiler produces produces bad scheme code for the following: ```idris total fun : Nat -> Nat fun k = ?fun_rhs total fun_proof : (x :...
On discord, a user reported a case where the compiler was producing scheme code that wouldn't compile. I've reduced the test case below. It appears that an internal pattern variable...