[Agda] Bit-wise XOR for Word64?

[Nils Anders Danielsson]

On 2020-09-29 19:04, David Banas wrote:
> Is there a bit-wise XOR operator for the Word64 type available in
> Agda?

If there isn't, then you can define it yourself using the FFI:

   open import Agda.Builtin.Word

   postulate
     _xor_ : Word64 → Word64 → Word64

   {-# FOREIGN GHC import qualified Data.Bits #-}
   {-# COMPILE GHC _xor_ = Data.Bits.xor #-}

   -- Optional: Postulated properties.

However, note that this definition of _xor_ does not compute at
compile-time. An alternative would be to define _xor_ using
primWord64ToNat and primWord64FromNat, but the resulting code would
presumably be less efficient.

-- 
/NAD