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
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-04-27. Fernando Chu, Fernando Chu, Fernando Chu and Fredrik Bakke. Reflection and solvers (#571).