From ded72f94b2b420b8725e9c6944bb585ebc8660bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Feb 2014 09:23:13 -0800 Subject: [PATCH] doc(todo): update todo list --- doc/todo.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/todo.md b/doc/todo.md index 66504c65d..d9e509d5d 100644 --- a/doc/todo.md +++ b/doc/todo.md @@ -14,4 +14,6 @@ To Do List - Independent type checker using a different programming language (e.g., F* or OCaml). - Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs. - Re-implement apply-tactic. -- Improve performance of `is_convertible` and `is_definitionally_equal` predicates +- Improve performance of `is_convertible` and `is_definitionally_equal` predicates. +- Create notation sets. We are currently all notation in a "single bag". +- Improve macro support, and allow users to provide arbitrary parser extensions using Lua.