From ea5eed796459b4eec7cf1b32f4e6c13d7b252d2d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jul 2020 14:36:54 -0700
Subject: [PATCH] fix: do not assume the constructor name prefix is the
 inductive type name

---
 src/frontends/lean/pp.cpp | 2 +-
 src/library/util.cpp      | 7 +++++++
 src/library/util.h        | 5 +++++
 3 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index bfc2042c2b..6e8a2d5fa5 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -685,7 +685,7 @@ static bool is_structure_instance(environment const & env, expr const & e, bool
     if (!is_constant(fn)) return false;
     name const & mk_name = const_name(fn);
     if (!is_constructor(env, mk_name)) return false;
-    name const & S       = mk_name.get_prefix();
+    name S = get_constructor_inductive_type(env, mk_name);
     if (!is_structure(env, S)) return false;
     /* If implicit arguments is true, and the structure has parameters, we should not
        pretty print using { ... }, because we will not be able to see the parameters. */
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 32cc91df33..e92388dc89 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -318,6 +318,13 @@ unsigned get_constructor_idx(environment const & env, name const & n) {
     lean_unreachable();
 }
 
+name get_constructor_inductive_type(environment const & env, name const & ctor_name) {
+    constant_info info  = env.get(ctor_name);
+    lean_assert(info.is_constructor());
+    constructor_val val = info.to_constructor_val();
+    return val.get_induct();
+}
+
 expr instantiate_lparam(expr const & e, name const & p, level const & l) {
     return instantiate_lparams(e, names(p), levels(l));
 }
diff --git a/src/library/util.h b/src/library/util.h
index 5fe6f42a04..6fa0e18c72 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -124,6 +124,11 @@ unsigned get_num_constructors(environment const & env, name const & n);
     \pre inductive::is_intro_rule(env, n) */
 unsigned get_constructor_idx(environment const & env, name const & n);
 
+/** \brief Given a constructor name, return the associated inductive type name.
+
+    \pre inductive::is_intro_rule(env, ctor_name) */
+name get_constructor_inductive_type(environment const & env, name const & ctor_name);
+
 /** \brief Given an expression \c e, return the number of arguments expected arguments.
 
     \remark This function counts the number of nested Pi's in \c e. Weak-head-normal-forms are computed for the type of \c e.