From df8b88dca2f8da1a422cb618cd476ef5be730546 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Jul 2014 12:08:54 -0700 Subject: [PATCH] chore(doc/todo): update todo list Signed-off-by: Leonardo de Moura --- doc/todo.md | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/doc/todo.md b/doc/todo.md index cc4a4184b8..788c7c019f 100644 --- a/doc/todo.md +++ b/doc/todo.md @@ -1,14 +1,7 @@ To Do List ---------- -- Universe polymorphism. -- Inductive datatypes. -- New representation for metavariables. -- New elaborator -- Add unification hints support in the Lean front-end. -- Improved extensible parser and pretty printer. -- Notation-sets for organizing user defined notation. +- Improved pretty printer. - Generic Tableaux prover. - [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework. - Independent type checker using a different programming language (e.g., F* or OCaml). -- New apply-tactic.