Swapped bitsEq Either ordering to be in the spirit of Right=success
commit12615d4d5d39558716914dfbb087129a9d5ac9c9
authorBenjamin Saunders <besaunde@sfu.ca>
dateThu 27 Dec 2012, 11:29 (14 years ago)
parentc3f27f7
lib/Prelude/Bits.idr+3−3
@@ -200,11 +200,11 @@ bitsEq' {n=n} x y with (nextBits n)
200200 | Bits64 = prim__eqB64 x y
201201
202202public
203−bitsEq : (x : Bits n) -> (y : Bits n) -> Either (x = y) (x = y -> _|_)
203+bitsEq : (x : Bits n) -> (y : Bits n) -> Either (x = y -> _|_) (x = y)
204204bitsEq (MkBits x) (MkBits y) =
205205 case (bitsEq' x y) of
206− 0 => Right uneq
207− _ => Left eq
206+ 0 => Left uneq
207+ _ => Right eq
208208 where
209209 postulate uneq : {x : Bits n} -> {y : Bits n} -> x = y -> _|_
210210 postulate eq : {x : Bits n} -> {y : Bits n} -> x = y