Rename ⟦_⟧ to float.

1 files changed, 5 insertions, 5 deletions

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))