André Videla
André Videla
After #165 is implemented, haskell types should have a couple of their types implemented and be available as specialized types. Here is a list of candidates: - [ ] `String`...
I would like to write down the different things we need to do until we can consider our effort in documenting typdefs over. This emerges from feedback I received from...
We should have a tutorial that displays common cases for typedefs and have a pool of snippets that users can readily copy paste in their own tools. This should be...
``` (name List (+ (name Nil 1) (name Cons (* (var x) (ref List))))) ``` should compile to ``` (name List (mu (Nil 1) (Cons (* (var 1) (var 0)))))...
The list type can be defined like this ``` (name List (mu (Nil 1) (Cons (* (var 1) (var 0))))) ``` But technically we could also allow ``` (name List...
In the API exposed for Idris, we expose the specialised types `TNat` and `TString` as well as counterparts that take a single type argument, but do not do anything with...
The `parseVect` function in the JSON Parser only check that the number fields in the json is as expected. However, we also need to check that each key has the...
``` eqTy : (tvars : Vect n (a : Type ** a -> a -> Bool)) -> (td : TDefR n) -> Ty' [] (map DPair.fst tvars) td -> Ty'...
The last PR allows to generate specialised type signatures in haskell but does not allow them to be serialized and deserialized. for example ```clojure (name intList (mu (Nil 1) (Cons...
Related to #169 and as a direct consequence of #172, the Haskell backend should prepend all constuctor patterns with the module name in order to avoid the following situation: tdef:...