fix(library/compiler/reduce_arity): bug at arity_was_reduced

It was retuning true for declarations such as
```lean
def f (n : Nat) :=
g._rarg n
```
It should only return true if the nested application is of the form
`f._rarg ...`
This commit is contained in:
Leonardo de Moura 2019-04-11 13:41:15 -07:00
parent be328bd8e9
commit b46f5f3eca

View file

@ -26,7 +26,7 @@ bool arity_was_reduced(comp_decl const & cdecl) {
expr const & f = get_app_fn(v);
if (!is_constant(f)) return false;
name const & n = const_name(f);
return is_reduce_arity_aux_fn(n);
return is_reduce_arity_aux_fn(n) && n.get_prefix() == cdecl.fst();
}
comp_decls reduce_arity(environment const & env, comp_decl const & cdecl) {