Idris2-boot
Idris2-boot copied to clipboard
edwinb
A dependently typed programming language, a successor to Idris
I was thinking of starting work on a JavaScript backend for Idris2. I have some preliminary work (AST and codegen) completed [on my fork](https://github.com/maxdeviant/Idris2/commits/js-backend), but I wanted to check in...
'addclause' client command fails to produce a meaningful definition for helpers under 'where' blocks
# Steps to Reproduce Attempting to generate a trivial definition for the `go` helper function (below) fails to produce meaningful results. The behaviour can also be reproduced by running idris2...
# Steps to Reproduce ``` module Test interface Foo a where bar : a -> {auto ok: ()} -> a ``` # Expected Behavior Typecheck (Like Idris1) # Observed Behavior...
This is a work in progress. Compilation currently fails with the following internal error: idris: Erasure.hs:lamToLet': unexpected input: vs = [{eta_4}], tm = Idris.Parser.case block in case block in mkLets...
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example...
# Steps to Reproduce Check ``` f : Ord k => SortedMap k v -> List (k, v) f m = case sortBy (\(x, _), (y, _) => compare x...
# Steps to Reproduce Check ``` f : A -> A f a = let x = record { fieldA = 1 } a in ?x ``` # Expected Behavior...
The compiler seems to struggle to unify interfaces with dependent types with their implementation. # Steps to Reproduce try to compile this module: ``` module Test data Dummy : (lbl...
Idris 2, version 0.1.0-19426ecd1 I've included a lambda of case and a lambdacase to show it's not specific to one. # Steps to Reproduce ```idris foo1 : () foo1 =...
It would be useful to have a way, in patterns, to check for the presence of a constructor without regard to its arguments. Currently given ```idris data Tree : Type...