Idris2

Idris2 copied to clipboard

These two functions are FFI-exported with the exact same type `Int -> PrimIO Int`, so I think it should be a reasonable expectation that their calling convention is the same....

gergoerdi

- [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 As far as I can tell, `absurd` is...

mars0i

Enable "library" generation in addition to "executable" generation for `-o` output.

3

At present, Idris2 has a number of ways in which the user can compile a given source file (e.g `X.idr`). For example, the user can write a package file, which...

AdamBrouwersHarries

The following program crashes with scheme exception "attempt to apply non-procedure 0": ``` bug : Int -> Bool bug a = let f = \y => case y == a...

bkomuves

A record in a namespace would make everything in the namespace public

1

# Steps to Reproduce ``` idris2 module Test namespace Foo record R where -- Comment this line and the following Use* doesn't compile data A : Type where B :...

91khr

Cannot incrementally build

2

# Summary `Exception: variable LibrariesC-45TextC-45Lexer-any is not bound` ## Reproduction 1. build idris2 from source, with `opts = "--inc chez"` in `idris2.ipkg`. 2. make install once more. 3. build fails:...

scarf005

Case tree is not strict enough, hard crash on scheme eval

2

I haven't tested it with yaffle (wrong laptop atm) but this is concerning: ```idris %default total boom : Nat === List () -> List () boom = \ eq =>...

gallais

Add source link for individual declaration on documentation

4

- [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  Add source link for each declaration like...

scarf005

Idris accepts matching on erased values

1

# Steps to Reproduce Tested on commit 6729fa8c8. Code: ```idris data Fin : Nat -> Type where FZ : Fin (S n) FS : Fin n -> Fin (S n)...

yellowsquid

Declaring data type in the `where` clause gives a unification error

5

Idris2 version (HEAD as of the time of raising the issue): ``` $ idris2 --version Idris 2, version 0.2.1-df4c454f4 ``` # Steps to Reproduce Here is the code: ``` module...

timmyjose