@@ -203,5 +203,8 @@ public
203203bitsEq : (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 (believe_me ())
207− _ => Left (believe_me ())
206+ 0 => Right uneq
207+ _ => Left eq
208+ where
209+ postulate uneq : {x : Bits n} -> {y : Bits n} -> x = y -> _|_
210+ postulate eq : {x : Bits n} -> {y : Bits n} -> x = y