From 6ffbb05118c6b855a7531f34b29d2fbd378a36e7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 Jul 2015 20:07:13 -0700
Subject: [PATCH] feat(library/definitional/no_confusion): add [unfold] hint to
 no_confusion

---
 src/library/definitional/no_confusion.cpp | 3 +++
 src/library/normalize.h                   | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp
index bda26b668..fb783272d 100644
--- a/src/library/definitional/no_confusion.cpp
+++ b/src/library/definitional/no_confusion.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/reducible.h"
 #include "library/constants.h"
+#include "library/normalize.h"
 
 namespace lean {
 static void throw_corrupted(name const & n) {
@@ -201,6 +202,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
     no_confusion_type_args.push_back(P);
     no_confusion_type_args.push_back(v1);
     no_confusion_type_args.push_back(v1);
+    unsigned unfold_hint_idx = no_confusion_type_args.size();
     expr no_confusion_type_app = mk_app(mk_constant(no_confusion_type_decl.get_name(), ls), no_confusion_type_args);
     expr type_former = Fun(type_former_args, no_confusion_type_app);
     // create cases_on
@@ -273,6 +275,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
                                       use_conv_opt);
     new_env = module::add(new_env, check(new_env, new_d));
     new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible);
+    new_env = add_unfold_hint(new_env, no_confusion_name, unfold_hint_idx);
     return add_protected(new_env, no_confusion_name);
 }
 }
diff --git a/src/library/normalize.h b/src/library/normalize.h
index 68c760d60..18ab7d975 100644
--- a/src/library/normalize.h
+++ b/src/library/normalize.h
@@ -41,6 +41,9 @@ expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const&
     Of course, kernel opaque constants are not unfolded.
 */
 environment add_unfold_hint(environment const & env, name const & n, list<unsigned> const & idxs, bool persistent = true);
+inline environment add_unfold_hint(environment const & env, name const & n, unsigned idx, bool persistent = true) {
+    return add_unfold_hint(env, n, to_list(idx), persistent);
+}
 environment erase_unfold_hint(environment const & env, name const & n, bool persistent = true);
 /** \brief Retrieve the hint added with the procedure add_unfold_hint. */
 list<unsigned> has_unfold_hint(environment const & env, name const & d);