This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Machine integers

module primitives.machine-integers where

open import elementary-number-theory.natural-numbers

open import foundation.identity-types
open import foundation.universe-levels

Idea

The Word64 type represents 64-bit machine words. Agda provides primitive functions to manipulate them.

Definitions

postulate
  Word64 : UU lzero

{-# BUILTIN WORD64 Word64 #-}

primitive
  primWord64ToNat : Word64 → ℕ
  primWord64FromNat : ℕ → Word64
  primWord64ToNatInjective :
    (a b : Word64) → primWord64ToNat a ＝ primWord64ToNat b → a ＝ b