From 568792d2890028fbf7d011393b6516af27cc8b2f Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Fri, 7 Jan 2022 09:59:41 +0000 Subject: Rename ⟦_⟧ to float. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Helium/Semantics/Denotational.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/Helium/Semantics') diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda index dce07e6..77786f1 100644 --- a/src/Helium/Semantics/Denotational.agda +++ b/src/Helium/Semantics/Denotational.agda @@ -167,14 +167,14 @@ copyMasked dest = module fun-sliceᶻ (≈ᶻ-trans : Transitive _≈ᶻ_) - (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧) + (round∘float : ∀ x → x ≈ᶻ round (float x)) (round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y) (0#-homo-round : round 0ℝ ≈ᶻ 0ℤ) (2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ)) (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x) where - open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ + open sliceᶻ ≈ᶻ-trans round∘float round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ signedSatQ : ∀ n → Function 1 (ℤ , _) (Bits (suc n) × Bool) signedSatQ n = declare ⦇ true ⦈ $ @@ -249,15 +249,15 @@ module _ module _ (≈ᶻ-trans : Transitive _≈ᶻ_) - (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧) + (round∘float : ∀ x → x ≈ᶻ round (float x)) (round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y) (0#-homo-round : round 0ℝ ≈ᶻ 0ℤ) (2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ)) (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x) where - open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ - open fun-sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ + open sliceᶻ ≈ᶻ-trans round∘float round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ + open fun-sliceᶻ ≈ᶻ-trans round∘float round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ vadd : VAdd → Procedure 2 (Beat , ElmtMask , _) vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x +ᶻ uint y)) -- cgit v1.2.3