Machine integers

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

Created on 2023-04-27.
Last modified on 2023-10-21.

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