Idris2
Idris2 copied to clipboard
idris-lang
A purely functional programming language with first class types
The only item remaining on the checklist for releases is: - [ ] Make libdocs and upload to idris-lang.org I can make the docs without any issues. However, there was...
# Steps to Reproduce Try typechecking ```idris module Foo %default total %prefix_record_projections off data NameKind = Name NameTy : NameKind -> Type NameTy Name = String record Person where name...
IDE mode works by sending/receiving messages on the wire in the form of s-expressions (lists, strings, bools, integers, symbols). Currently, almost all the commands are implemented by delegating the processing...
This issue looks really similar to #3158, but this issue, I think, is different. The #3158 is about particular backend, but this feature is about C FFI, available to (and...
Today, I was in need of `Alternative` for `Either e` (well, only the `` part, but that's the whole point). Yet, of course, there is no such thing, as we...
- [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 The IDE protocol currently supports a...
# Description Hi team I needed a citation for my MSc Project, and I found that GH supports citation files, so I thought I could create a PR for this...
Hi. I've asked this on nixpkgs (https://github.com/NixOS/nixpkgs/issues/119175) but I imagine I'd find more answers here. I'm looking to get the `idris.with-packages` behaviour that I'm used to in nix. I was...
Found while looking at the code interactively generated by case splitting in #2242. ```idris %default total g : Not Bool g () impossible f : Void f = g True...
# Steps to Reproduce Consider the folllowing code: ```idris import Data.Nat %default total conc : List a -> List a -> List a conc xs [] = xs conc xs...
Metadata
Owner
Metadata
A purely functional programming language with first class types