------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on machine words
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Word64.Properties where
import Data.Nat.Base as ℕ
open import Data.Bool.Base using (Bool)
open import Data.Word64.Base using (_≈_; toℕ; Word64; _<_)
import Data.Nat.Properties as ℕ
open import Relation.Nullary.Decidable.Core using (map′; ⌊_⌋)
open import Relation.Binary
using ( _⇒_; Reflexive; Symmetric; Transitive; Substitutive
; Decidable; DecidableEquality; IsEquivalence; IsDecEquivalence
; Setoid; DecSetoid; StrictTotalOrder)
import Relation.Binary.Construct.On as On using (decidable; strictTotalOrder)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; cong; sym; trans; subst)
open import Relation.Binary.PropositionalEquality.Properties
using (setoid; decSetoid)
------------------------------------------------------------------------
-- Primitive properties
open import Agda.Builtin.Word.Properties
renaming (primWord64ToNatInjective to toℕ-injective)
public
------------------------------------------------------------------------
-- Properties of _≈_
≈⇒≡ : _≈_ ⇒ _≡_
≈⇒≡ = toℕ-injective _ _
≈-reflexive : _≡_ ⇒ _≈_
≈-reflexive = cong toℕ
≈-refl : Reflexive _≈_
≈-refl = refl
≈-sym : Symmetric _≈_
≈-sym = sym
≈-trans : Transitive _≈_
≈-trans = trans
≈-subst : ∀ {ℓ} → Substitutive _≈_ ℓ
≈-subst P x≈y p = subst P (≈⇒≡ x≈y) p
infix 4 _≈?_
_≈?_ : Decidable _≈_
x ≈? y = toℕ x ℕ.≟ toℕ y
≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
{ refl = λ {i} → ≈-refl {i}
; sym = λ {i j} → ≈-sym {i} {j}
; trans = λ {i j k} → ≈-trans {i} {j} {k}
}
≈-setoid : Setoid _ _
≈-setoid = record
{ isEquivalence = ≈-isEquivalence
}
≈-isDecEquivalence : IsDecEquivalence _≈_
≈-isDecEquivalence = record
{ isEquivalence = ≈-isEquivalence
; _≟_ = _≈?_
}
≈-decSetoid : DecSetoid _ _
≈-decSetoid = record
{ isDecEquivalence = ≈-isDecEquivalence
}
------------------------------------------------------------------------
-- Properties of _≡_
infix 4 _≟_
_≟_ : DecidableEquality Word64
x ≟ y = map′ ≈⇒≡ ≈-reflexive (x ≈? y)
≡-setoid : Setoid _ _
≡-setoid = setoid Word64
≡-decSetoid : DecSetoid _ _
≡-decSetoid = decSetoid _≟_
------------------------------------------------------------------------
-- Boolean equality test.
infix 4 _==_
_==_ : Word64 → Word64 → Bool
w₁ == w₂ = ⌊ w₁ ≟ w₂ ⌋
------------------------------------------------------------------------
-- Properties of _<_
infix 4 _<?_
_<?_ : Decidable _<_
_<?_ = On.decidable toℕ ℕ._<_ ℕ._<?_
<-strictTotalOrder-≈ : StrictTotalOrder _ _ _
<-strictTotalOrder-≈ = On.strictTotalOrder ℕ.<-strictTotalOrder toℕ
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4