From 80e3da052661733a24d154996a38a8da9444d90c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Jul 2015 16:30:00 -0700 Subject: [PATCH] fix(library/util): fixes #751 --- src/library/util.cpp | 15 ++++++++++++++- tests/lean/run/751.lean | 4 ++++ 2 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/751.lean diff --git a/src/library/util.cpp b/src/library/util.cpp index 164812520..b75adee67 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -118,6 +118,11 @@ bool has_lift_decls(environment const & env) { return has_constructor(env, get_lift_up_name(), get_lift_name(), 2); } +// n is considered to be recursive if it is an inductive datatype and +// 1) It has a constructor that takes n as an argument +// 2) It is part of a mutually recursive declaration, and some constructor +// of an inductive datatype takes another inductive datatype from the +// same declaration as an argument. bool is_recursive_datatype(environment const & env, name const & n) { optional decls = inductive::is_inductive_decl(env, n); if (!decls) @@ -127,7 +132,15 @@ bool is_recursive_datatype(environment const & env, name const & n) { expr type = inductive::intro_rule_type(intro); while (is_pi(type)) { if (find(binding_domain(type), [&](expr const & e, unsigned) { - return is_constant(e) && const_name(e) == n; })) { + if (is_constant(e)) { + name const & c = const_name(e); + for (auto const & d : std::get<2>(*decls)) { + if (inductive::inductive_decl_name(d) == c) + return true; + } + } + return false; + })) { return true; } type = binding_body(type); diff --git a/tests/lean/run/751.lean b/tests/lean/run/751.lean new file mode 100644 index 000000000..6f1dc45c2 --- /dev/null +++ b/tests/lean/run/751.lean @@ -0,0 +1,4 @@ +inductive foo (A : Type) := +| intro : foo A → foo A +with bar : Type := +| intro : bar A