From f74e8288bde4c0dc474e7c959c9d515397c09eca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 7 Nov 2015 17:24:17 -0800
Subject: [PATCH] refactor(library/congr_lemma_manager): API

---
 src/frontends/lean/builtin_cmds.cpp |  6 +++---
 src/library/congr_lemma_manager.h   | 29 +++++++++++++++--------------
 2 files changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 7ca817e79..4e639105f 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -1299,9 +1299,9 @@ static environment congr_lemma_cmd(parser & p) {
     for (auto k : r->get_arg_kinds()) {
         if (!first) out << ", "; else first = false;
         switch (k) {
-        case congr_lemma_manager::congr_arg_kind::Fixed: out << "fixed"; break;
-        case congr_lemma_manager::congr_arg_kind::Eq:    out << "eq";    break;
-        case congr_lemma_manager::congr_arg_kind::Cast:  out << "cast";  break;
+        case congr_arg_kind::Fixed: out << "fixed"; break;
+        case congr_arg_kind::Eq:    out << "eq";    break;
+        case congr_arg_kind::Cast:  out << "cast";  break;
         }
     }
     out << "]\n";
diff --git a/src/library/congr_lemma_manager.h b/src/library/congr_lemma_manager.h
index 9236734a4..f9849a087 100644
--- a/src/library/congr_lemma_manager.h
+++ b/src/library/congr_lemma_manager.h
@@ -10,6 +10,20 @@ Author: Leonardo de Moura
 #include "library/fun_info_manager.h"
 
 namespace lean {
+enum class congr_arg_kind { Fixed, Eq, Cast };
+
+class congr_lemma {
+    expr                 m_type;
+    expr                 m_proof;
+    list<congr_arg_kind> m_arg_kinds;
+public:
+    congr_lemma(expr const & type, expr const & proof, list<congr_arg_kind> const & ks):
+        m_type(type), m_proof(proof), m_arg_kinds(ks) {}
+    expr const & get_type() const { return m_type; }
+    expr const & get_proof() const { return m_proof; }
+    list<congr_arg_kind> const & get_arg_kinds() const { return m_arg_kinds; }
+};
+
 class congr_lemma_manager {
     struct imp;
     std::unique_ptr<imp> m_ptr;
@@ -23,20 +37,7 @@ public:
         we want the argumet s to remain fixed. */
     congr_lemma_manager(app_builder & b, fun_info_manager & fm, bool ignore_inst_implicit = true);
     ~congr_lemma_manager();
-
-    enum class congr_arg_kind { Fixed, Eq, Cast };
-
-    class result {
-        expr                 m_type;
-        expr                 m_proof;
-        list<congr_arg_kind> m_arg_kinds;
-    public:
-        result(expr const & type, expr const & proof, list<congr_arg_kind> const & ks):
-            m_type(type), m_proof(proof), m_arg_kinds(ks) {}
-        expr const & get_type() const { return m_type; }
-        expr const & get_proof() const { return m_proof; }
-        list<congr_arg_kind> const & get_arg_kinds() const { return m_arg_kinds; }
-    };
+    typedef congr_lemma result;
 
     optional<result> mk_congr_simp(expr const & fn);
     optional<result> mk_congr_simp(expr const & fn, unsigned nargs);