@@ -171,8 +171,7 @@ bitsSDiv' {n=n} x y with (nextBits n)
171171 | Bits32 = prim__sdivB32 x y
172172 | Bits64 = prim__sdivB64 x y
173173
174−public
175−partial
174+public partial
176175bitsSDiv : Bits n -> Bits n -> Bits n
177176bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
178177
@@ -184,8 +183,7 @@ bitsUDiv' {n=n} x y with (nextBits n)
184183 | Bits32 = prim__udivB32 x y
185184 | Bits64 = prim__udivB64 x y
186185
187−public
188−partial
186+public partial
189187bitsUDiv : Bits n -> Bits n -> Bits n
190188bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
191189
@@ -197,8 +195,7 @@ bitsSRem' {n=n} x y with (nextBits n)
197195 | Bits32 = prim__sremB32 x y
198196 | Bits64 = prim__sremB64 x y
199197
200−public
201−partial
198+public partial
202199bitsSRem : Bits n -> Bits n -> Bits n
203200bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
204201
@@ -210,8 +207,7 @@ bitsURem' {n=n} x y with (nextBits n)
210207 | Bits32 = prim__uremB32 x y
211208 | Bits64 = prim__uremB64 x y
212209
213−public
214−partial
210+public partial
215211bitsURem : Bits n -> Bits n -> Bits n
216212bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
217213
@@ -271,12 +267,26 @@ public
271267bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
272268bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0
273269
270+instance Eq (Bits n) where
271+ (==) = bitsEq
272+
273+instance Ord (Bits n) where
274+ (<) = bitsLt
275+ (<=) = bitsLte
276+ (>=) = bitsGte
277+ (>) = bitsGt
278+ compare x y = if x `bitsLt` y
279+ then LT
280+ else if x `bitsEq` y
281+ then EQ
282+ else GT
283+
274284public
275285bitsToStr : Bits n -> String
276286bitsToStr {n=n} x = helper n x
277287 where
278288 helper : Nat -> Bits n -> String
279− helper (S x) b = (if bitsAnd (bitsShl (intToBits 1) (intToBits (cast x))) b `bitsEq` (intToBits 0)
289+ helper (S x) b = (if bitsAnd (bitsShl (intToBits 1) (intToBits (cast x))) b == (intToBits 0)
280290 then "0"
281291 else "1"
282292 ) ++ helper x b