@@ -56,20 +56,20 @@ copy { n } = MkBuffer . prim__copy ( bitsFromNat n ) . realBuffer
5656%assert_total
5757public
5858peekBufferNative : Buffer ( m + n ) ->
59− ( offset : Fin ( n + 1 ) ) ->
59+ ( offset : Fin ( S n ) ) ->
6060 Buffer m
6161peekBufferNative ( MkBuffer real ) =
6262 MkBuffer . prim__peekBufferNative real . bitsFromFin
6363
6464public
6565peekBufferLE : Buffer ( m + n ) ->
66− ( offset : Fin ( n + 1 ) ) ->
66+ ( offset : Fin ( S n ) ) ->
6767 Buffer m
6868peekBufferLE = peekBufferNative
6969
7070public
7171peekBufferBE : Buffer ( m + n ) ->
72− ( offset : Fin ( n + 1 ) ) ->
72+ ( offset : Fin ( S n ) ) ->
7373 Buffer m
7474peekBufferBE = peekBufferNative
7575
@@ -108,7 +108,7 @@ appendBufferBE = appendBufferNative
108108
109109peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->
110110 Buffer ( m + n ) ->
111− ( offset : Fin ( n + 1 ) ) ->
111+ ( offset : Fin ( S n ) ) ->
112112 a
113113peekBits prim ( MkBuffer real ) = prim real . bitsFromFin
114114
@@ -129,18 +129,18 @@ appendBits { n } prim ( MkBuffer real ) count =
129129%assert_total
130130public
131131peekBits8Native : Buffer ( 1 + n ) ->
132− ( offset : Fin ( n + 1 ) ) ->
132+ ( offset : Fin ( S n ) ) ->
133133 Bits8
134134peekBits8Native = peekBits { m = 1 } prim__peekB8Native
135135
136136%assert_total
137137public
138−peekBits8LE : Buffer ( 1 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits8
138+peekBits8LE : Buffer ( 1 + n ) -> ( offset : Fin ( S n ) ) -> Bits8
139139peekBits8LE = peekBits { m = 1 } prim__peekB8LE
140140
141141%assert_total
142142public
143−peekBits8BE : Buffer ( 1 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits8
143+peekBits8BE : Buffer ( 1 + n ) -> ( offset : Fin ( S n ) ) -> Bits8
144144peekBits8BE = peekBits { m = 1 } prim__peekB8BE
145145
146146-- Append count repetitions of a Bits8 to a Buffer
@@ -173,20 +173,20 @@ appendBits8BE = appendBits prim__appendB8BE
173173%assert_total
174174public
175175peekBits16Native : Buffer ( 2 + n ) ->
176− ( offset : Fin ( n + 1 ) ) ->
176+ ( offset : Fin ( S n ) ) ->
177177 Bits16
178178peekBits16Native = peekBits { m = 2 } prim__peekB16Native
179179
180180-- Read a little-endian Bits16 from a Buffer starting at offset
181181%assert_total
182182public
183−peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits16
183+peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16
184184peekBits16LE = peekBits { m = 2 } prim__peekB16LE
185185
186186-- Read a big-endian Bits16 from a Buffer starting at offset
187187%assert_total
188188public
189−peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits16
189+peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16
190190peekBits16BE = peekBits { m = 2 } prim__peekB16BE
191191
192192-- Append count repetitions of a Bits16 in native byte order to a Buffer
@@ -220,20 +220,20 @@ appendBits16BE = appendBits prim__appendB16BE
220220%assert_total
221221public
222222peekBits32Native : Buffer ( 4 + n ) ->
223− ( offset : Fin ( n + 1 ) ) ->
223+ ( offset : Fin ( S n ) ) ->
224224 Bits32
225225peekBits32Native = peekBits { m = 4 } prim__peekB32Native
226226
227227-- Read a little-endian Bits32 from a Buffer starting at offset
228228%assert_total
229229public
230−peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits32
230+peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32
231231peekBits32LE = peekBits { m = 4 } prim__peekB32LE
232232
233233-- Read a big-endian Bits32 from a Buffer starting at offset
234234%assert_total
235235public
236−peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits32
236+peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32
237237peekBits32BE = peekBits { m = 4 } prim__peekB32BE
238238
239239-- Append count repetitions of a Bits32 in native byte order to a Buffer
@@ -267,20 +267,20 @@ appendBits32BE = appendBits prim__appendB32BE
267267%assert_total
268268public
269269peekBits64Native : Buffer ( 8 + n ) ->
270− ( offset : Fin ( n + 1 ) ) ->
270+ ( offset : Fin ( S n ) ) ->
271271 Bits64
272272peekBits64Native = peekBits { m = 8 } prim__peekB64Native
273273
274274-- Read a little-endian Bits64 from a Buffer starting at offset
275275%assert_total
276276public
277−peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits64
277+peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64
278278peekBits64LE = peekBits { m = 8 } prim__peekB64LE
279279
280280-- Read a big-endian Bits64 from a Buffer starting at offset
281281%assert_total
282282public
283−peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits64
283+peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64
284284peekBits64BE = peekBits { m = 8 } prim__peekB64BE
285285
286286-- Append count repetitions of a Bits64 in native byte order to a Buffer