Idris2
Idris2 copied to clipboard
idris-lang
A purely functional programming language with first class types
# Steps to Reproduce Type check the following markdown ````idris ```idris x : Nat x = "" ``` * some text ```idris y : Nat y = "" ``` ````...
In incremental compilation mode, some, but not all metas are compiled. This inconsistency leads to problems for codegen backends which require a definition for all used symbols. I noticed this...
check if a linux implementation uses glibc to decide whether to load "glibc.so.6" or "glibc.so"
- [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 want to be able to annotate the...
# Steps to Reproduce I was trying this with a simple list and a NonEmpty predicate, but here's a minimal example without it: ```hs total f : (a, List a)...
While trying to understand the differences between Agda's and Idris's positivity checkers, I came across [Andreas Abel's message from 2012](https://lists.chalmers.se/pipermail/agda/2012/004297.html), which passes the totality checker when translated to Idris: ```idris...
# Description This PR immortalizes objects whose reference counter has reached its maximum value and makes them excluded from GC. This immortalization is used to make the following improvements. *...
This follows on from #2930. Now that we've had a version bump, we can bind `fromTTImp`, `fromName`, and `fromDecls` in base.
- [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 Making the signature of output of `((:interpret String)...
After loading a file the Idris2 changes working directory to one level higher and same time keeps reference to the original working directory leading to error `Source file X is...
Metadata
Owner
Metadata
A purely functional programming language with first class types