@@ -206,10 +206,7 @@ bitsLt' {n=n} x y with (nextBits n)
206206
207207public
208208bitsLt : (x : Bits n) -> (y : Bits n) -> Bool
209−bitsLt (MkBits x) (MkBits y) =
210− case (bitsLt' x y) of
211− 0 => False
212− _ => True
209+bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0
213210
214211bitsLte' : (x : nextBits n) -> (y : nextBits n) -> Int
215212bitsLte' {n=n} x y with (nextBits n)
@@ -220,10 +217,7 @@ bitsLte' {n=n} x y with (nextBits n)
220217
221218public
222219bitsLte : (x : Bits n) -> (y : Bits n) -> Bool
223−bitsLte (MkBits x) (MkBits y) =
224− case (bitsLte' x y) of
225− 0 => False
226− _ => True
220+bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0
227221
228222bitsEq' : (x : nextBits n) -> (y : nextBits n) -> Int
229223bitsEq' {n=n} x y with (nextBits n)
@@ -234,10 +228,7 @@ bitsEq' {n=n} x y with (nextBits n)
234228
235229public
236230bitsEq : (x : Bits n) -> (y : Bits n) -> Bool
237−bitsEq (MkBits x) (MkBits y) =
238− case (bitsEq' x y) of
239− 0 => False
240− _ => True
231+bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0
241232
242233bitsGte' : (x : nextBits n) -> (y : nextBits n) -> Int
243234bitsGte' {n=n} x y with (nextBits n)
@@ -248,10 +239,7 @@ bitsGte' {n=n} x y with (nextBits n)
248239
249240public
250241bitsGte : (x : Bits n) -> (y : Bits n) -> Bool
251−bitsGte (MkBits x) (MkBits y) =
252− case (bitsGte' x y) of
253− 0 => False
254− _ => True
242+bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0
255243
256244bitsGt' : (x : nextBits n) -> (y : nextBits n) -> Int
257245bitsGt' {n=n} x y with (nextBits n)
@@ -262,7 +250,4 @@ bitsGt' {n=n} x y with (nextBits n)
262250
263251public
264252bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
265−bitsGt (MkBits x) (MkBits y) =
266− case (bitsGt' x y) of
267− 0 => False
268− _ => True
253+bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0