Machine integers

Content created by Fredrik Bakke and Fernando Chu.

Created on 2023-04-27.
Last modified on 2023-05-01.

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 → primWord64ToNat a ＝ primWord64ToNat b → a ＝ b

Recent changes