From f527b931d850276d28830d356f2f1fde6209d759 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Sep 2013 23:07:40 -0700 Subject: [PATCH] Update todo.md --- doc/todo.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/todo.md b/doc/todo.md index 761ebd492..e05c3fcc9 100644 --- a/doc/todo.md +++ b/doc/todo.md @@ -13,7 +13,7 @@ To Do List - Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs. - Higher-Order unification and matching. - Rewriter (and Rewriter Combinators). -- MCSat framework. +- [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework. - Implement independent type checker using a different programming language (e.g., OCaml). - Add `match` construct in `expr`. - Add inductive datatype (families) in the environment. It will be a new kind of object.