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

chore: remove unnecessary inline

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-23 15:26:22 -07:00
parent c232e9e1c8
commit aa77c0a651
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Data/ByteArray/Basic.lean
View file

@ -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 := #[] }