git.iko.soy/Idris-dev
on master help sign in
More concise (and less fragile) boolean comparison wrappers
9909d70Benjamin Saunders
lib/Prelude/Bits.idr+5−20
compare with master
unifiedsplit
@@ -206,10 +206,7 @@ bitsLt' {n=n} x y with (nextBits n)
206
206
207public
207public
208bitsLt : (x : Bits n) -> (y : Bits n) -> Bool
208bitsLt : (x : Bits n) -> (y : Bits n) -> Bool
209−bitsLt (MkBits x) (MkBits y) =
209+bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0
210− case (bitsLt' x y) of
211− 0 => False
212− _ => True
213
210
214bitsLte' : (x : nextBits n) -> (y : nextBits n) -> Int
211bitsLte' : (x : nextBits n) -> (y : nextBits n) -> Int
215bitsLte' {n=n} x y with (nextBits n)
212bitsLte' {n=n} x y with (nextBits n)
@@ -220,10 +217,7 @@ bitsLte' {n=n} x y with (nextBits n)
220
217
221public
218public
222bitsLte : (x : Bits n) -> (y : Bits n) -> Bool
219bitsLte : (x : Bits n) -> (y : Bits n) -> Bool
223−bitsLte (MkBits x) (MkBits y) =
220+bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0
224− case (bitsLte' x y) of
225− 0 => False
226− _ => True
227
221
228bitsEq' : (x : nextBits n) -> (y : nextBits n) -> Int
222bitsEq' : (x : nextBits n) -> (y : nextBits n) -> Int
229bitsEq' {n=n} x y with (nextBits n)
223bitsEq' {n=n} x y with (nextBits n)
@@ -234,10 +228,7 @@ bitsEq' {n=n} x y with (nextBits n)
234
228
235public
229public
236bitsEq : (x : Bits n) -> (y : Bits n) -> Bool
230bitsEq : (x : Bits n) -> (y : Bits n) -> Bool
237−bitsEq (MkBits x) (MkBits y) =
231+bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0
238− case (bitsEq' x y) of
239− 0 => False
240− _ => True
241
232
242bitsGte' : (x : nextBits n) -> (y : nextBits n) -> Int
233bitsGte' : (x : nextBits n) -> (y : nextBits n) -> Int
243bitsGte' {n=n} x y with (nextBits n)
234bitsGte' {n=n} x y with (nextBits n)
@@ -248,10 +239,7 @@ bitsGte' {n=n} x y with (nextBits n)
248
239
249public
240public
250bitsGte : (x : Bits n) -> (y : Bits n) -> Bool
241bitsGte : (x : Bits n) -> (y : Bits n) -> Bool
251−bitsGte (MkBits x) (MkBits y) =
242+bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0
252− case (bitsGte' x y) of
253− 0 => False
254− _ => True
255
243
256bitsGt' : (x : nextBits n) -> (y : nextBits n) -> Int
244bitsGt' : (x : nextBits n) -> (y : nextBits n) -> Int
257bitsGt' {n=n} x y with (nextBits n)
245bitsGt' {n=n} x y with (nextBits n)
@@ -262,7 +250,4 @@ bitsGt' {n=n} x y with (nextBits n)
262
250
263public
251public
264bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
252bitsGt : (x : Bits n) -> (y : Bits n) -> Bool
265−bitsGt (MkBits x) (MkBits y) =
253+bitsGt (MkBits x) (MkBits y) = bitsGt' x y /= 0
266− case (bitsGt' x y) of
267− 0 => False
268− _ => True