------------------------------------------------------------------------
-- The Agda standard library
--
-- Machine words: basic type and conversion functions
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Word64.Base where
 
open import Algebra.Core using (Op₂)
open import Data.Nat.Base as ℕ using (ℕ)
open import Function.Base using (_on_; _∘₂′_)
open import Level using (zero)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
------------------------------------------------------------------------
-- Re-export built-ins publicly
 
open import Agda.Builtin.Word public
  using (Word64)
  renaming
  ( primWord64ToNat   to toℕ
  ; primWord64FromNat to fromℕ
  )
 
liftOp₂ : Op₂ ℕ → Op₂ Word64
liftOp₂ op = fromℕ ∘₂′ op on toℕ
 
infix  _≈_
_≈_ : Rel Word64 zero
_≈_ = _≡_ on toℕ
 
infix  _<_
_<_ : Rel Word64 zero
_<_ = ℕ._<_ on toℕ
 
infix  _≤_
_≤_ : Rel Word64 zero
_≤_ = ℕ._≤_ on toℕ