disco

disco copied to clipboard

`2f(n)` parses as `2 * f * n`

3

This definition yields a type error: ``` f : N -> N f(0) f(n+1) = 2f(n) + 3 ``` It is accepted if we add a `*` sign in between...

byorgey

Way to provide "hints" for existentials

2

For example, consider the following function definition + accompanying claim that the function is onto: ``` !!! ∀ n:N. ∃ m:N. f3(m) == n f3 : N -> N f3(n)...

byorgey

Use a random structure generation library to test parse/pretty-print round trip

2

This should probably wait until after #61 , otherwise I bet it is going to be a lot of tedious work to get it set up all over again.

byorgey

It's inconsistent that Cartesian product for sets requires `>

byorgey

Patterns and let in container comprehension qualifiers

3

Haskell supports pattern bindings and `let` expressions in list comprehensions, *e.g.* ``` [ (q,q+1) | Just y

byorgey

Randomness

6

It would be nice to incorporate randomness into the language somehow. There is a large design space to think about. 1. We could simply make the language semantics nondeterministic, so...

byorgey

Shadowing in list comprehensions

6

``` Disco> :type [ x | x

byorgey

If we have e.g. `A : Set(N)` it would be neat to be able to write something like `forall x in A. blah(x)`.

byorgey

Haddock-like output for disco

1

We should be able to generate web pages with documentation, especially for standard library modules. The idea would be to generate an HTML listing of functions and types defined in...

byorgey

Parse arguments to `:load` the same way the shell does

2

If you try to `:load` something from a path that has spaces, it stops prior to the space and claims it can't find the given module. We could maybe use...

byorgey