@@ -182,6 +182,33 @@ bitsToStr' {n=n} x with (nextBits n)
182182bitsToStr : Bits n -> String
183183bitsToStr (MkBits x) = bitsToStr' x
184184
185+-- TODO: Proofy comparisons via postulates
186+bitsLt' : (x : nextBits n) -> (y : nextBits n) -> Int
187+bitsLt' {n=n} x y with (nextBits n)
188+ | Bits8 = prim__ltB8 x y
189+ | Bits16 = prim__ltB16 x y
190+ | Bits32 = prim__ltB32 x y
191+ | Bits64 = prim__ltB64 x y
192+
193+bitsLt : (x : Bits n) -> (y : Bits n) -> Bool
194+bitsLt (MkBits x) (MkBits y) =
195+ case (bitsLt' x y) of
196+ 0 => False
197+ _ => True
198+
199+bitsLte' : (x : nextBits n) -> (y : nextBits n) -> Int
200+bitsLte' {n=n} x y with (nextBits n)
201+ | Bits8 = prim__lteB8 x y
202+ | Bits16 = prim__lteB16 x y
203+ | Bits32 = prim__lteB32 x y
204+ | Bits64 = prim__lteB64 x y
205+
206+bitsLte : (x : Bits n) -> (y : Bits n) -> Bool
207+bitsLte (MkBits x) (MkBits y) =
208+ case (bitsLte' x y) of
209+ 0 => False
210+ _ => True
211+
185212bitsEq' : (x : nextBits n) -> (y : nextBits n) -> Int
186213bitsEq' {n=n} x y with (nextBits n)
187214 | Bits8 = prim__eqB8 x y
@@ -194,3 +221,29 @@ bitsEq (MkBits x) (MkBits y) =
194221 case (bitsEq' x y) of
195222 0 => False
196223 _ => True
224+
225+bitsGte' : (x : nextBits n) -> (y : nextBits n) -> Int
226+bitsGte' {n=n} x y with (nextBits n)
227+ | Bits8 = prim__gteB8 x y
228+ | Bits16 = prim__gteB16 x y
229+ | Bits32 = prim__gteB32 x y
230+ | Bits64 = prim__gteB64 x y
231+
232+bitsGte : (x : Bits n) -> (y : Bits n) -> Bool
233+bitsGte (MkBits x) (MkBits y) =
234+ case (bitsGte' x y) of
235+ 0 => False
236+ _ => True
237+
238+bitsGt' : (x : nextBits n) -> (y : nextBits n) -> Int
239+bitsGt' {n=n} x y with (nextBits n)
240+ | Bits8 = prim__gtB8 x y
241+ | Bits16 = prim__gtB16 x y
242+ | Bits32 = prim__gtB32 x y
243+ | Bits64 = prim__gtB64 x y
244+
245+bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
246+bitsGt (MkBits x) (MkBits y) =
247+ case (bitsGt' x y) of
248+ 0 => False
249+ _ => True