michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/util): fixes #751

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-28 16:30:00 -07:00
parent 6805aab344
commit 80e3da0526
2 changed files with 18 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/library/util.cpp
View file

@ -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<inductive::inductive_decls> 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);

4
tests/lean/run/751.lean Normal file
View file

@ -0,0 +1,4 @@
inductive foo (A : Type) :=
| intro : foo A → foo A
with bar : Type :=
| intro : bar A