From aa77c0a651af243e8cc8a68e9430162684bf2f63 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Oct 2019 15:26:22 -0700 Subject: [PATCH] chore: remove unnecessary `inline` --- library/Init/Data/ByteArray/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 := #[] }