Machine integers

Content created by Fredrik Bakke, Egbert Rijke and Fernando Chu.

Created on 2023-04-27.
Last modified on 2024-04-11.

module primitives.machine-integers where
Imports 
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

Recent changes