Idris2

Idris2 copied to clipboard

# Steps to Reproduce - Idris 2, version 0.7.0-e02ebcab6 (installed with [pack](https://github.com/stefan-hoeck/idris2-pack)) - clone https://github.com/freddi301/idris-2-ui/tree/6f70fc6c7dbbe1790a1488d68dd334b53c892764 - run `watch-build .sh` - mistype any named parameter in `style = s{ grw =...

freddi301

Type checking issue with Idris2 Load instruction in dependent context

1

I've encountered a potential type checking bug in Idris2. The issue arises specifically with the Load instruction when it takes an Int argument and operates within a dependent type context....

weiserhase

Type information is lost/changed when inlining a function (and it's not clear why)

5

Note: I'm not sure whether this is a bug or I don't fully understand how some language feature is supposed to work (I'm currently learning Idris). If you find it's...

JavierGelatti

# Steps to Reproduce Consider the following code: ``` %default total %tcinline f : Nat -> a -> a f Z x = x f (S k) x = f...

AntonPing

This is a complex one. I'm not sure if it's a bug in Idris, Bazel (the build system), or my use of Bazel, but ohad asked me to raise an...

joelberkeley

- [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. ## Motivation Currently, using the linear network API, you can...

Alex1005a

Totality checker fails to recognize missing cases on irrelevant parameter in irrelevant function

1

```idris total 0 unlift : (0 x : Bool) -> (x == x) = True unlift True = Refl -- unlift False = Refl ``` The totality/coverage checker fails to...

Adowrath

[ refactor ] ScopedSnocList: WIP

5

# Description We are going to take again a turn to solve [TODO](https://github.com/idris-lang/Idris2/pull/3151/files#diff-cf8968d49c872d0b0e8b7d8300722726d7ee15ab1780104b7799afa8f8c1009aR23), related to the usage of SnocList at Scope. This change is heavily intrusive and its older attempt...

GulinSS

- [ ] 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 Let's allow to generate only es6 code...

srghma

# 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...

dunhamsteve