iacore
# Steps to Reproduce Compile the following code ``` %foreign "javascript:xyz" prim__run_next_tick : IO a -> IO a ``` 1. `set -x IDRIS2_INC_CGS chez` or `export IDRIS2_INC_CGS=chez` 2. `idris2 --cg...
## Example 1 ``` poly : IO a -> IO a poly = id hole_to_fill : IO (forall a . IO a -> IO a) hole_to_fill = pure poly ```...
## The proposal 1: Add `Rational` type 2: Add related helper functions to `Data.Rational` 3: Make decimal literals use `fromRational` (like `fromInteger`) 4: Add an interface for non-total division Related:...
Try run `0.1 + 0.2 + 0.3` in REPL. ``` Main> 0.1 + 0.2 + 0.3 Error: Can't find an implementation for FromDouble Integer. (Interactive):1:1--1:4 1 | 0.1 + 0.2...
- [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 Since Idris2 model effects as Monad, it's possible...
- [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 Sometimes there are two or more ipkg files...
# Steps to Reproduce ``` data Foo : Type -> Type where MkFoo : Foo a data F : (Type -> Type) -> Type where MkF : v a ->...
## Summary Currently, a term of `SortedMap` hides the term of `Ord k` it depends on. I suggest that sorted data types should depend on `Ord k` at type level,...
## Summary Currently, the command `idris2` can only compile programs as executable objects. However, this is not useful, since in some cases we want to generate libraries in another programming...
I added a Nim script to patch cimgui and build `libcimgui.a`. However, I don't know how to run this script on build. (I did it manually and it worked fine)