Remove bitstring addition.

2 files changed, 3 insertions, 8 deletions

diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 6cf25ec..5027784 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -167,8 +167,6 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x)
     where
 
-    infix 5 _+ᵇ_
-
     open divmod ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round
     open 2^n≢0 ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0
 
@@ -178,6 +176,3 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     sliceᶻ (suc n) (suc i) z = sliceᶻ n i ((z div 2ℤ) {2≢0})
       where
       2≢0 = map-False (≈ᶻ-trans (*ᶻ-identityʳ 2ℤ)) (2^n≢0 1)
-
-    _+ᵇ_ : ∀ {n} → Op₂ (Bits n)
-    x +ᵇ y = sliceᶻ _ zero (uint x +ᶻ uint y)
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index 0739d28..c2a4d6e 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -150,11 +150,11 @@ module _
   open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ
 
   vadd : VAdd → Procedure 2 (Beat , ElmtMask , _)
-  vadd d = vec-op₂ d _+ᵇ_
+  vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x +ᶻ uint y))
 
   vhsub : VHSub → Procedure 2 (Beat , ElmtMask , _)
-  vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ (suc (toℕ esize)) (suc zero) (int x +ᶻ -ᶻ int y))
+  vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ _ (suc zero) (int x +ᶻ -ᶻ int y))
     where open VHSub d ; int = Bool.if unsigned then uint else sint
 
   vmul : VMul → Procedure 2 (Beat , ElmtMask , _)
-  vmul d = vec-op₂ d (λ x y → sliceᶻ (toℕ _) zero (sint x *ᶻ sint y))
+  vmul d = vec-op₂ d (λ x y → sliceᶻ _ zero (sint x *ᶻ sint y))