diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp index 0faf4728df..e245ee9319 100644 --- a/src/library/compiler/extern_attribute.cpp +++ b/src/library/compiler/extern_attribute.cpp @@ -170,9 +170,11 @@ static optional 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(); - else if (is_mpz(arity)) return optional(); // ignore big nums - else return optional(unbox(arity)); + if (is_scalar(arity)) return optional(); // none + // arity is (some v) + arity = cnstr_get(arity, 0); + if (is_scalar(arity)) return optional(unbox(arity)); + return optional(); // ignore big nums } optional get_extern_constant_arity(environment const & env, name const & c) {