André Videla

This but for typedefs https://twitter.com/ray_codes_stuff/status/1300783285707182080 Project: https://github.com/hediet/vscode-debug-visualizer/blob/master/extension/README.md This would be slightly different since it would display both the runtime value _and_ the type it matches. It would be a great...

Nesting `name` doesn't work

2

The following should work but does not ```clj (name blah (* (name char byte) (list byte) )) ```

Add a "syntax AST" for typedefs

9

All #133 #164 #163 #172 require changes to the AST but do not necessarily change the semantics of the language. This means it would be possible to write a new...

https://github.com/typedefs/typedefs/blob/fb909be7589509df0b78b29d43e35673f5177514/src/Typedefs/Strings.idr This file has been removed and the functions have been placed in `Typedefs.Typedefs`. This has been done to satisfy nix to build typedefs, indeed, with the file and the...

PureScript backend

1

Add support for a purescript backend with both term definition and type definitions. Could probably be a straight port from the Haskell backend

```clojure (specialised Int) (name MyInt (mu (MkInt Int))) ``` outputs ``` data MyInt = MkInt MyInt ``` instead of ``` data MyInt = MkInt Int ```

during #227 I noticed the serialisation functions for binary weren't actually used. Given the flexibility of the interface maybe this is the opportunity to use quickcheck. maybe after `TermWrite` is...

After #165 is implemented, specialized types should be usable. However there is no api to defined specialized types with custom user-defined types. Something like (this is user code) ```Haskell data...

Typedefs is a large project, it has multiple dependencies and uses a large spectrum of Idris's features. This makes it a compelling case for testing and benchmarking the compiler. I...

Fix parser on identifiers which aren't type applications but use references

1

```clojure (specialised Int) (specialised String) (specialised Date) (name Amount (mu (MkAmount Int))) (name Hash (mu (MkHash String))) (name Transaction (* Hash Date Amount)) ``` this fails on `Hash` at the...