Idris2-boot
Idris2-boot copied to clipboard
edwinb
A dependently typed programming language, a successor to Idris
Major change: - Support Mathematical Operators and Arrows as Symbols/Operators From [a commit](https://github.com/edwinb/Idris2/commit/1a4f42425963cc414997d33fc9f4b8bac9fc1fbf) in this repo: > While we're at it, Idris 1 supports unicode identifiers (although we don't encourage...
# Steps to Reproduce Stick this code at the bottom of Prelude.idr: ```idris interface Semigroup a => VerifiedSemigroup a where semigroupOpIsAssociative : (l, c, r : a) -> l (c...
For example, if I want to prove that a function returns a well-typed output on any file. What should the input type be? `Data.Buffer` has IO interface and can't be...
This has to be cleaned up a bit before it's ready for merging. I'm open to any and all bikeshedding about the "Coredris" name or the actual sexp syntax (like...
# Steps to Reproduce ``` badEq : ((x: Nat) -> Nat) = ((1 x:Nat) -> Nat) badEq = Refl ``` # Expected Behavior The term should not typecheck because this...
Just did a git pull (at 21507e64f38c3ac4a1f0fafce7fa7e5c1f59ec1d), and running "make install" fails with: ``` ... Type checking ./Idris/IDEMode/REPL.idr Type checking ./Idris/Main.idr ./Idris/Main.idr:49:15-21: | 49 | Nothing => setPrefix yprefix |...
