From 45ef10e2c18bbfb2cd05bb370f1cbbe270d3d38e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Feb 2014 17:01:30 -0800 Subject: [PATCH] doc(todo): update todo list --- doc/todo.md | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/doc/todo.md b/doc/todo.md index 6126cce21..14c234f25 100644 --- a/doc/todo.md +++ b/doc/todo.md @@ -1,9 +1,17 @@ To Do List ---------- -- Add Sigma-types. -- Define natural numbers, lists, inductive datatypes from first principles. The goal is to use the HOL/Isabelle approach. +- Add heterogeneous equality back into the kernel. +- Finish Sigma-type support. +- Build Nat and List theories. +- Fix usability issues identified when formalizing optional and sum types. +- Add unification hints support in the Lean front-end. +- Improve simp tactic interface (more configuration options). +- Add ssreflect-like rewrite commands. +- Add record-type (as syntax sugar for Sigma-types). +- Implement inductive datatypes and recursive function package from first principles. The goal is to use the HOL/Isabelle approach. - 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). - Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs. +- Re-implement apply-tactic.