@@ -32,16 +32,16 @@ natToBits' : machineTy n -> Nat -> machineTy n
3232natToBits' a O = a
3333natToBits' {n=n} a x with n
3434 natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__intToB8 1)) x'
35− natToBits' a (S x') | S O = natToBits' (prim__addB16 a (prim__intToB16 1)) x'
36− natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__intToB32 1)) x'
37− natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__intToB64 1)) x'
35+ natToBits' a (S x') | S O = natToBits' {n = S O} (prim__addB16 a (prim__intToB16 1)) x'
36+ natToBits' a (S x') | S (S O) = natToBits' {n=S (S O)} (prim__addB32 a (prim__intToB32 1)) x'
37+ natToBits' a (S x') | S (S (S k)) = natToBits' {n = S (S (S k))} (prim__addB64 a (prim__intToB64 1)) x'
3838
3939natToBits : Nat -> machineTy n
4040natToBits {n=n} x with n
41− | O = natToBits' (prim__intToB8 0) x
42− | S O = natToBits' (prim__intToB16 0) x
43− | S (S O) = natToBits' (prim__intToB32 0) x
44− | S (S (S _)) = natToBits' (prim__intToB64 0) x
41+ | O = natToBits' {n=O} (prim__intToB8 0) x
42+ | S O = natToBits' {n=S O} (prim__intToB16 0) x
43+ | S (S O) = natToBits' {n=S (S O)} (prim__intToB32 0) x
44+ | S (S (S k)) = natToBits' {n=S (S (S k))} (prim__intToB64 0) x
4545
4646getPad : Nat -> machineTy n
4747getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
@@ -111,7 +111,8 @@ shiftRightLogical' {n=n} x c with n
111111
112112public
113113shiftRightLogical : Bits n -> Bits n -> Bits n
114−shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)
114+shiftRightLogical {n} (MkBits x) (MkBits y)
115+ = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
115116
116117shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
117118shiftRightArithmetic' {n=n} x c with (nextBytes n)
@@ -133,7 +134,7 @@ and' {n=n} x y with n
133134
134135public
135136and : Bits n -> Bits n -> Bits n
136−and (MkBits x) (MkBits y) = MkBits (and' x y)
137+and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
137138
138139or' : machineTy n -> machineTy n -> machineTy n
139140or' {n=n} x y with n
@@ -144,7 +145,7 @@ or' {n=n} x y with n
144145
145146public
146147or : Bits n -> Bits n -> Bits n
147−or (MkBits x) (MkBits y) = MkBits (or' x y)
148+or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
148149
149150xor' : machineTy n -> machineTy n -> machineTy n
150151xor' {n=n} x y with n
@@ -153,6 +154,7 @@ xor' {n=n} x y with n
153154 | S (S O) = prim__xorB32 x y
154155 | S (S (S _)) = prim__xorB64 x y
155156
157+{-
156158public
157159xor : Bits n -> Bits n -> Bits n
158160xor (MkBits x) (MkBits y) = MkBits (xor' x y)
@@ -437,3 +439,5 @@ bitsToStr x = pack (helper last x)
437439
438440instance Show (Bits n) where
439441 show = bitsToStr
442+
443+-}