Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100644 49 lines (42 sloc) 1.969 kb
4a53940 Initial version
eb authored
1 Short term things to do:
2
6687a33 Add 'displayName'
eb authored
3 * Allow holes in pattern matching definitions
6c8845d Added IOvor
eb authored
4 * Need an easier way of updating a context with an input file
5 (currently have to create a shell, then load, then create a new
6 shell if you want to modify the context further)
e032ecc Fix haddock errors
eb authored
7 * Improve error messages!
6c2bfb1 expandCon implemented
eb authored
8 * Recursive functions shouldn't reduce at type level.
9b5b488 Pattern covering generation and checking
eb authored
9 * Either better than Monad m? Define an Error type.
583bcba Added 'exists' tactic
eb authored
10 * Fix naming bug --- terms of form t1 -> t2 automatically give t1 the
11 name X, which can clash. Particularly a problem in data type declarations.
5c7172d Some preparing for writing out files as raw TT, other tweaks
eb authored
12 * Current naive proof state representation is far too slow. Come up
13 with something better.
4a53940 Initial version
eb authored
14 * Keep track of level in proof state.
3f6e388 Removing the need to 'solve' or 'keepSolving' everywhere
eb authored
15 * Keep track of binding level in context, and check at point of use.
5c7172d Some preparing for writing out files as raw TT, other tweaks
eb authored
16 * Allow dump of global context to disk, for fast reloading.
4a53940 Initial version
eb authored
17 * Syntax for equality.
18 * Elimination with a motive.
19 * Unit tests - at least check nat.tt, vect.tt, JM equality,
20 primitives, simple staging, compiler.
21 * More readable high level language for function definition. Really
22 just has to use tactic engine to translate simple case expressions into
23 D-case calls.
24 * Separate API into several files for clarity.
25 * Allow call <fn args> _ in raw terms; i.e. allow the typechecker to
26 spot recursive calls, rather than needing a tactic to do so.
27 * Finish compiler by:
28 - Finding a method of exporting primitive types
29 - Implement compilation of D-Case
30
31 Things which could be done to the library, in no particular order
32 (other than the order I thought of them in...):
33
34 * A higher level dependently typed language might be useful (e.g. like
35 Coq's language). If not useful, at least fun :).
36 * Namespace management.
37 * Some useful error messages from the Parsec parsers would be nice.
38 * Proper type universes, of some form.
e45dc0e Added a basic standard library path
eb authored
39 * Generate DRec and DNoConfusion as well as DElim/DCase.
40 * Build in Sigma types? (At least a nicer syntax?)
41 * Infix operators, especially = would be nice.
4a53940 Initial version
eb authored
42
43 Tactics:
44
45 * Injectivity.
46 * Discriminate.
e45dc0e Added a basic standard library path
eb authored
47 * Inversion.
4a53940 Initial version
eb authored
48
Something went wrong with that request. Please try again.