Idris2
Idris2 copied to clipboard
idris-lang
A purely functional programming language with first class types
I've found an inconsistency bug: ```idris %default total A : Type A = ((), Nat) Z : A Z = ((), 0) S : A -> A S a =...
Linearity seems ubiquitous enough that it would be useful to have special syntax for it. ``` A #-> B -- as sugar for (1 _ : A) -> B ```...
I regularly come across "Ambiguous elaboration", followed by a number of options. When I disambiguate to each of these options, only one type checks. I would consider this a bug...
# Steps to Reproduce ``` import Data.List.Elem %default total mapMaybeList : (s -> s') -> List (Maybe s) -> List (Maybe s') mapMaybeList f xs = map (map f) xs...
At the moment if all alternatives of `IAlternative` with `FirstSuccess` rule are failing, only the last error is printed, which can be misleading.
Hi. I'm trying to implement a custom backend but the output of `getCompileData` is really hard to read, due to the `Show` instances trying to be too clever. I have...
# Steps to Reproduce Unified examples gist (e.g., for the future regression test) [can be found here](https://gist.github.com/buzden/454d70dfc61fbdb335eb213491b91174). Consider a primitive elaboration script that just quotates a type and logs it:...
# Steps to Reproduce Compile this with `idris2 --cg javascript test.idr` ``` main : IO () main = do putStrLn "1" putStrLn "2" ``` # Expected Behavior ``` 1 2...
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example...
## Summary Implement a means of passing idris-managed byte buffers to the C FFI. The clearest way to do this would be to coerce the Buffer into an AnyPtr. ##...
Metadata
Owner
Metadata
A purely functional programming language with first class types