Idris2

Idris2 copied to clipboard

RefC Backend + makeString memory problems

6

The way strings are handled as (char *) poses problems. I don't see an easy way out. Here is the deal: ## Problem 1. The function `Value* makeString(char*)` creates a...

vfrinken

Memory leak in idris2_readLine

6

Idris appears to be leaking memory in FFI on scheme. This was first noticed because the LSP process was growing as I was working on Idris. Repeatedly reloading a touched...

dunhamsteve

Add Rational Number to standard library

5

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

iacore

Confusing eror with conflicting defaulting interfaces

1

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

iacore

Hole is not fully supported inside rewrite

1

# Steps to Reproduce Run the following code (taken from https://idris2.readthedocs.io/en/latest/proofs/propositional.html#rewrite replacing `a` inside `rewrite` by `?a`) ``` p1: Nat -> Type p1 x = (x=2) testRewrite: (y=x) -> (p1...

ngeiswei

# Steps to Reproduce Run the following: ```idris2 loop : Nat -> PrimIO () loop Z w = MkIORes () w loop (S k) w = let MkIORes () w2...

stefan-hoeck

Incorrect rejection of erased irrefutable patterns

6

(spotted by locria) # Steps to Reproduce ```idris f : (0 x : (a,b)) -> Nat f x = let 0 (u,v) = x in 0 ``` # Expected Behavior...

ohad

No example of non-positional record construction in documentation

1

https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#records doesn't show the syntax for constructing a record with non-positional arguments: ``` fred : Person fred = MkPerson "Fred" "Joe" "Bloggs" 30 ``` Luckily, I've found https://github.com/idris-lang/Idris2/pull/607#issuecomment-682456667 which shows...

gergoerdi

Structured concurrency primitives

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 Since Idris2 model effects as Monad, it's possible...

iacore

Support fallback to a non-foreign function if not implemented for the current codegen

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 I propose that there should be a mechanism...

gwerbin