Tillmann Rendel

Implement section syntax or parameterized modules.

3

To avoid long repetitive parameter lists.

Improve name representation

1

Currently, most names a string from the user program plus an integer for freshening. We fear that comparing the strings takes too much time. We discusses some ideas for improvement:...

Type inference should be optional

1

See discussion of #69.

The `.ghci` file should define a `:test` command that runs unit tests from ghci. This can be done by something like the following: ``` cmdTests args = :def test cmdTests...

We should support explicit type annotations of the form `term : term`. The dynamic semantics would be to reduce to the left-hand term and ignore the annotation. The static semantics...

Integrate with SugarJ

4

Integrate with the SugarFOmega variant of SugarJ in order to create SugarPTS. See [seba--/sugarj](https://github.com/seba--/sugarj) and [florenzen/sugarj](https://github.com/florenzen/sugarj).

Support Fω* syntax

2

Currently, only generic PTS syntax is supported, but for literate programming (at least), it would be better to support the actual Fω\* syntax.

Test support for #line pragmas

2

EDITED: Test the support for #line pragmas. Tillmann introduced this in 7b4a4e516ddfa805a282d98693595d12470b7fc1 (see comment below) for better integration with code generators such as `lhs2tex --newcode`.

Better test case generation

1

Our test case generator is too stupid to check cool properties (see discussion of #23). We should write better Arbitrary instances. Maybe SmallCheck could also help?