diff --git a/library/Init/Data/ByteArray/Basic.lean b/library/Init/Data/ByteArray/Basic.lean index ed2dd9147c..b99f4f3a28 100644 --- a/library/Init/Data/ByteArray/Basic.lean +++ b/library/Init/Data/ByteArray/Basic.lean @@ -16,7 +16,7 @@ attribute [extern "lean_byte_array_mk"] ByteArray.mk attribute [extern "lean_byte_array_data"] ByteArray.data namespace ByteArray -@[extern c inline "lean_mk_empty_byte_array(#1)"] +@[extern "lean_mk_empty_byte_array"] def mkEmpty (c : @& Nat) : ByteArray := { data := #[] }