From 58783a2d3b949cb16b862b40bba57454623d8564 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Feb 2019 16:51:23 -0800
Subject: [PATCH] fix(library/compiler/extern_attribute): bug at
 `get_given_arity`

---
 src/library/compiler/extern_attribute.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

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<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) {