@@ -55,32 +55,20 @@ copy { n } = MkBuffer . prim__copy ( bitsFromNat n ) . realBuffer
5555-- (i.e. create a view of a subset of the Buffer)
5656%assert_total
5757public
58−peekBufferNative : Buffer ( m + n ) ->
59− ( offset : Fin ( S n ) ) ->
60− Buffer m
61−peekBufferNative ( MkBuffer real ) =
62− MkBuffer . prim__peekBufferNative real . bitsFromFin
63−
64−public
65−peekBufferLE : Buffer ( m + n ) ->
66− ( offset : Fin ( S n ) ) ->
67− Buffer m
68−peekBufferLE = peekBufferNative
69−
70−public
71−peekBufferBE : Buffer ( m + n ) ->
72− ( offset : Fin ( S n ) ) ->
73− Buffer m
74−peekBufferBE = peekBufferNative
58+peekBuffer : Buffer ( m + n ) ->
59+ ( offset : Fin ( S n ) ) ->
60+ Buffer m
61+peekBuffer ( MkBuffer real ) =
62+ MkBuffer . prim__peekBuffer real . bitsFromFin
7563
7664-- Append count repetitions of a Buffer to another Buffer
7765%assert_total
7866public
79−appendBufferNative : Buffer n ->
80− ( count : Nat ) ->
81− Buffer m ->
82− Buffer ( n + m * count )
83−appendBufferNative { n } { m } ( MkBuffer input ) count =
67+appendBuffer : Buffer n ->
68+ ( count : Nat ) ->
69+ Buffer m ->
70+ Buffer ( n + m * count )
71+appendBuffer { n } { m } ( MkBuffer input ) count =
8472 MkBuffer . app . realBuffer
8573 where
8674 nBits : Bits64
@@ -89,21 +77,7 @@ appendBufferNative { n } { m } ( MkBuffer input ) count =
8977 mBits = bitsFromNat m
9078 cBits : Bits64
9179 cBits = bitsFromNat count
92− app = prim__appendBufferNative input nBits cBits mBits
93−
94−public
95−appendBufferLE : Buffer n ->
96− ( count : Nat ) ->
97− Buffer m ->
98− Buffer ( n + m * count )
99−appendBufferLE = appendBufferNative
100−
101−public
102−appendBufferBE : Buffer n ->
103− ( count : Nat ) ->
104− Buffer m ->
105− Buffer ( n + m * count )
106−appendBufferBE = appendBufferNative
80+ app = prim__appendBuffer input nBits cBits mBits
10781
10882
10983peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->