Skip to content

Commit 2fb5c4b

Browse files
committed
move capacity forward
1 parent 9d6af78 commit 2fb5c4b

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Binary/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,7 @@ export Encode (put)
145145
attribute [specialize] Encode.put
146146

147147
@[always_inline]
148-
def Put.run (capacity : Nat := 128) : Put → ByteArray := fun x =>
148+
def Put.run (x : Put) (capacity : Nat := 128) : ByteArray :=
149149
Prod.snd <$> x (ByteArray.emptyWithCapacity capacity)
150150

151151
@[always_inline]

0 commit comments

Comments
 (0)