From b46f5f3ecad0f828d1d826eaf258ddba520f99ac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Apr 2019 13:41:15 -0700 Subject: [PATCH] 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 ...` --- src/library/compiler/reduce_arity.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/compiler/reduce_arity.cpp b/src/library/compiler/reduce_arity.cpp index 9414509d11..659e7231df 100644 --- a/src/library/compiler/reduce_arity.cpp +++ b/src/library/compiler/reduce_arity.cpp @@ -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) {