@@ -203,5 +203,8 @@ public
203bitsEq : (x : Bits n) -> (y : Bits n) -> Either (x = y) (x = y -> _|_)
203bitsEq : (x : Bits n) -> (y : Bits n) -> Either (x = y) (x = y -> _|_)
204bitsEq (MkBits x) (MkBits y) =
204bitsEq (MkBits x) (MkBits y) =
205 case (bitsEq' x y) of
205 case (bitsEq' x y) of
206− 0 => Right (believe_me ())
206+ 0 => Right uneq
207− _ => Left (believe_me ())
207+ _ => Left eq
209+ postulate uneq : {x : Bits n} -> {y : Bits n} -> x = y -> _|_
210+ postulate eq : {x : Bits n} -> {y : Bits n} -> x = y