max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/extern_attribute): bug at get_given_arity

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-11 16:51:23 -08:00
parent d877bdf546
commit 58783a2d3b
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/compiler/extern_attribute.cpp
View file

@ -170,9 +170,11 @@ static optional<unsigned> get_given_arity(environment const & env, name const &
lean_assert(is_extern_constant_core(env, c));
extern_attr_data_value v = get_extern_attr().get(env, c)->m_value;
object * arity = cnstr_get(v.raw(), 0);
if (is_scalar(arity)) return optional<unsigned>();
else if (is_mpz(arity)) return optional<unsigned>(); // ignore big nums
else return optional<unsigned>(unbox(arity));
if (is_scalar(arity)) return optional<unsigned>(); // none
// arity is (some v)
arity = cnstr_get(arity, 0);
if (is_scalar(arity)) return optional<unsigned>(unbox(arity));
return optional<unsigned>(); // ignore big nums
}
optional<unsigned> get_extern_constant_arity(environment const & env, name const & c) {