From e01da4d4e51f8a136ba7fc1c98e255488f138e53 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Oct 2013 09:37:53 -0700 Subject: [PATCH] doc(todo): 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 c50a798b5..62108bb41 100644 --- a/doc/todo.md +++ b/doc/todo.md @@ -11,7 +11,7 @@ To Do List - We use an off-the-shelf embedded language such as [Lua](http://www.lua.org). - We use Lean itself. - Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs. -- Higher-Order unification and matching. +- ~~Higher-Order unification and matching~~. - Rewriter (and Rewriter Combinators). - [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework. - Implement independent type checker using a different programming language (e.g., OCaml).